diff -r d6ce4ce20422 -r 6424f74fd9d4 src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Sat Nov 20 18:15:09 2021 +0100 +++ b/src/Pure/Thy/latex.scala Sat Nov 20 18:58:23 2021 +0100 @@ -73,7 +73,7 @@ if (file_pos.isEmpty) Nil else List("\\endinput\n", position(Markup.FILE, file_pos)) - class Output + class Output(options: Options) { def latex_output(latex_text: Text): String = apply(latex_text) @@ -87,7 +87,7 @@ XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body) def latex_heading(kind: String, body: Text): Text = - XML.enclose("%\n\\isamarkup" + kind + "{", "%\n}\n", body) + XML.enclose("%\n\\" + options.string("document_heading_prefix") + kind + "{", "%\n}\n", body) def latex_body(kind: String, body: Text): Text = latex_environment("isamarkup" + kind, body)