clarified signature: allow to change options in instances of Document_Build.Engine;
authorwenzelm
Sat, 05 Nov 2022 12:29:22 +0100
changeset 76450 107d8203fbd7
parent 76449 739edaad4f42
child 76451 87cd8506e000
clarified signature: allow to change options in instances of Document_Build.Engine;
src/Pure/Thy/document_build.scala
src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/document_build.scala	Sat Nov 05 12:27:53 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Sat Nov 05 12:29:22 2022 +0100
@@ -229,7 +229,7 @@
 
       isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
 
-      val comment_latex = options.bool("document_comment_latex")
+      val comment_latex = latex_output.options.bool("document_comment_latex")
       if (!comment_latex) {
         Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir)
       }
--- a/src/Pure/Thy/latex.scala	Sat Nov 05 12:27:53 2022 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Nov 05 12:29:22 2022 +0100
@@ -157,7 +157,7 @@
     if (file_pos.isEmpty) Nil
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
-  class Output(options: Options) {
+  class Output(val options: Options) {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
     def latex_macro0(name: String, optional_argument: String = ""): Text =