forked from Isabelle_DOF/Isabelle_DOF
clarified DOF.options: hard-wired document_comment_latex always uses LaTeX version of comment.sty
This commit is contained in:
parent
73299941ad
commit
700a9bbfee
|
@ -19,8 +19,6 @@
|
||||||
%% you need to download lipics.cls from
|
%% you need to download lipics.cls from
|
||||||
%% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
|
%% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
|
||||||
%% and add it manually to the praemble.tex and the ROOT file.
|
%% and add it manually to the praemble.tex and the ROOT file.
|
||||||
%% Moreover, the option "document_comment_latex=true" needs to be set
|
|
||||||
%% in the ROOT file.
|
|
||||||
%%
|
%%
|
||||||
%% All customization and/or additional packages should be added to the file
|
%% All customization and/or additional packages should be added to the file
|
||||||
%% preamble.tex.
|
%% preamble.tex.
|
||||||
|
|
|
@ -63,4 +63,6 @@ object DOF {
|
||||||
// Isabelle/DOF release artifacts
|
// Isabelle/DOF release artifacts
|
||||||
|
|
||||||
val artifact_host = "artifacts.logicalhacking.com"
|
val artifact_host = "artifacts.logicalhacking.com"
|
||||||
|
|
||||||
|
def options(opts: Options): Options = opts + "document_comment_latex"
|
||||||
}
|
}
|
||||||
|
|
|
@ -44,7 +44,8 @@ object DOF_Document_Build
|
||||||
dir: Path,
|
dir: Path,
|
||||||
doc: Document_Build.Document_Variant): Document_Build.Directory =
|
doc: Document_Build.Document_Variant): Document_Build.Directory =
|
||||||
{
|
{
|
||||||
val latex_output = new Latex_Output(context.options)
|
val options = DOF.options(context.options)
|
||||||
|
val latex_output = new Latex_Output(options)
|
||||||
val directory = context.prepare_directory(dir, doc, latex_output)
|
val directory = context.prepare_directory(dir, doc, latex_output)
|
||||||
|
|
||||||
// produced by alternative presentation hook (workaround for missing Toplevel.present_theory)
|
// produced by alternative presentation hook (workaround for missing Toplevel.present_theory)
|
||||||
|
@ -62,7 +63,7 @@ object DOF_Document_Build
|
||||||
// copy Isabelle/DOF LaTeX templates
|
// copy Isabelle/DOF LaTeX templates
|
||||||
val template_dir = isabelle_dof_dir + Path.explode("document-templates")
|
val template_dir = isabelle_dof_dir + Path.explode("document-templates")
|
||||||
// TODO: error handling in case 1) template does not exist or 2) root.tex does already exist
|
// TODO: error handling in case 1) template does not exist or 2) root.tex does already exist
|
||||||
val template = Long_Name.base_name(context.options.string("dof_template"))
|
val template = Long_Name.base_name(options.string("dof_template"))
|
||||||
Isabelle_System.copy_file(
|
Isabelle_System.copy_file(
|
||||||
template_dir + Path.explode("root-" + template + ".tex"),
|
template_dir + Path.explode("root-" + template + ".tex"),
|
||||||
directory.doc_dir + Path.explode("root.tex"))
|
directory.doc_dir + Path.explode("root.tex"))
|
||||||
|
@ -75,7 +76,7 @@ object DOF_Document_Build
|
||||||
.foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file))
|
.foreach(sty => Isabelle_System.copy_file(sty, directory.doc_dir.file))
|
||||||
|
|
||||||
// create ontology.sty
|
// create ontology.sty
|
||||||
val ontologies = DOF.explode_ontologies(context.options.string("dof_ontologies"))
|
val ontologies = DOF.explode_ontologies(options.string("dof_ontologies"))
|
||||||
File.write(directory.doc_dir + Path.explode("ontologies.tex"),
|
File.write(directory.doc_dir + Path.explode("ontologies.tex"),
|
||||||
ontologies.map(name => "\\usepackage{DOF-" + Long_Name.base_name(name) + "}\n").mkString)
|
ontologies.map(name => "\\usepackage{DOF-" + Long_Name.base_name(name) + "}\n").mkString)
|
||||||
|
|
||||||
|
|
|
@ -68,8 +68,7 @@ object DOF_Mkroot
|
||||||
File.write(root_path,
|
File.write(root_path,
|
||||||
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
|
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ +
|
||||||
options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """
|
options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """
|
||||||
+ quote(DOF.implode_ontologies(ontologies)) + """, dof_template = """ + quote(template)
|
+ quote(DOF.implode_ontologies(ontologies)) + """, dof_template = """ + quote(template) + """]
|
||||||
+ """, document_comment_latex = true]
|
|
||||||
(*theories [document = false]
|
(*theories [document = false]
|
||||||
A
|
A
|
||||||
B*)
|
B*)
|
||||||
|
|
|
@ -174,7 +174,7 @@ section \<open>Miscellaneous NEWS and Notes\<close>
|
||||||
|
|
||||||
text \<open>
|
text \<open>
|
||||||
\<^item> Document preparation: there are many new options etc. that might help
|
\<^item> Document preparation: there are many new options etc. that might help
|
||||||
to fine-tune DOF output, e.g. \<^system_option>\<open>document_comment_latex\<close>.
|
to fine-tune DOF output, e.g. \<^system_option>\<open>document_heading_prefix\<close>.
|
||||||
|
|
||||||
\<^item> ML: Theory_Data / Generic_Data: "val extend = I" has been removed;
|
\<^item> ML: Theory_Data / Generic_Data: "val extend = I" has been removed;
|
||||||
obsolete since Isabelle2021.
|
obsolete since Isabelle2021.
|
||||||
|
|
Reference in New Issue