# HG changeset patch
# User wenzelm
# Date 1667647762 -3600
# Node ID 107d8203fbd7a1bb8e147820627b69eea48b2ce5
# Parent  739edaad4f421b600b8e9de7d74d92a248604e8d
clarified signature: allow to change options in instances of Document_Build.Engine;

diff -r 739edaad4f42 -r 107d8203fbd7 src/Pure/Thy/document_build.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)
       }
diff -r 739edaad4f42 -r 107d8203fbd7 src/Pure/Thy/latex.scala
--- 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 =