diff --git a/src/document-templates/root-lipics-v2021-UNSUPPORTED.tex b/src/document-templates/root-lipics-v2021-UNSUPPORTED.tex index 76f78cfe..74b984f7 100644 --- a/src/document-templates/root-lipics-v2021-UNSUPPORTED.tex +++ b/src/document-templates/root-lipics-v2021-UNSUPPORTED.tex @@ -19,8 +19,6 @@ %% you need to download lipics.cls from %% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ %% 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 %% preamble.tex. diff --git a/src/scala/dof.scala b/src/scala/dof.scala index f1c90662..5f2593d6 100644 --- a/src/scala/dof.scala +++ b/src/scala/dof.scala @@ -63,4 +63,6 @@ object DOF { // Isabelle/DOF release artifacts val artifact_host = "artifacts.logicalhacking.com" + + def options(opts: Options): Options = opts + "document_comment_latex" } diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index b699d1e1..40cdfac0 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -44,7 +44,8 @@ object DOF_Document_Build dir: Path, 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) // produced by alternative presentation hook (workaround for missing Toplevel.present_theory) @@ -62,7 +63,7 @@ object DOF_Document_Build // copy Isabelle/DOF LaTeX 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 - 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( template_dir + Path.explode("root-" + template + ".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)) // 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"), ontologies.map(name => "\\usepackage{DOF-" + Long_Name.base_name(name) + "}\n").mkString) diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala index c0c78f43..fc066d0d 100644 --- a/src/scala/dof_mkroot.scala +++ b/src/scala/dof_mkroot.scala @@ -68,8 +68,7 @@ object DOF_Mkroot File.write(root_path, "session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(DOF.session) + """ + options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """ - + quote(DOF.implode_ontologies(ontologies)) + """, dof_template = """ + quote(template) - + """, document_comment_latex = true] + + quote(DOF.implode_ontologies(ontologies)) + """, dof_template = """ + quote(template) + """] (*theories [document = false] A B*) diff --git a/src/tests/Isabelle2021-1.thy b/src/tests/Isabelle2021-1.thy index 314d45d9..6a8759db 100644 --- a/src/tests/Isabelle2021-1.thy +++ b/src/tests/Isabelle2021-1.thy @@ -174,7 +174,7 @@ section \Miscellaneous NEWS and Notes\ text \ \<^item> Document preparation: there are many new options etc. that might help - to fine-tune DOF output, e.g. \<^system_option>\document_comment_latex\. + to fine-tune DOF output, e.g. \<^system_option>\document_heading_prefix\. \<^item> ML: Theory_Data / Generic_Data: "val extend = I" has been removed; obsolete since Isabelle2021.