src/Pure/Thy/latex.scala

--- a/src/Pure/Thy/latex.scala	Tue Nov 23 20:46:40 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Tue Nov 23 21:02:13 2021 +0100
@@ -116,10 +116,15 @@
     def latex_environment(name: String, body: Text): Text =
       XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body)
 
-    def latex_heading(kind: String, pos: Position.T, body: Text): Text =
-      XML.enclose("%\n\\" + options.string("document_heading_prefix") + kind + "{", "%\n}\n", body)
+    def latex_heading(kind: String, props: Properties.T, body: Text): Text =
+    {
+      val prefix =
+        "%\n\\" + options.string("document_heading_prefix") + kind +
+        Markup.Optional_Argument.get(props)
+      XML.enclose(prefix + "{", "%\n}\n", body)
+    }
 
-    def latex_body(kind: String, pos: Position.T, body: Text): Text =
+    def latex_body(kind: String, props: Properties.T, body: Text): Text =
       latex_environment("isamarkup" + kind, body)
 
     def latex_delim(name: String, body: Text): Text =
@@ -178,9 +183,9 @@
           case XML.Elem(Markup.Latex_Environment(name), body) =>
             traverse(latex_environment(name, body))
           case XML.Elem(markup @ Markup.Latex_Heading(kind), body) =>
-            traverse(latex_heading(kind, markup.position_properties, body))
+            traverse(latex_heading(kind, markup.properties, body))
           case XML.Elem(markup @ Markup.Latex_Body(kind), body) =>
-            traverse(latex_body(kind, markup.position_properties, body))
+            traverse(latex_body(kind, markup.properties, body))
           case XML.Elem(Markup.Latex_Delim(name), body) =>
             traverse(latex_delim(name, body))
           case XML.Elem(Markup.Latex_Tag(name), body) =>