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)