clarified signature: allow to change options in instances of Document_Build.Engine;
--- 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 =