more symbolic latex_output via XML;

--- a/src/Pure/PIDE/markup.ML	Sat Nov 20 13:53:34 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 20 18:15:09 2021 +0100
@@ -153,6 +153,8 @@
   val latex_macro0N: string val latex_macro0: string -> T
   val latex_macroN: string val latex_macro: string -> T
   val latex_environmentN: string val latex_environment: string -> T
+  val latex_headingN: string val latex_heading: string -> T
+  val latex_bodyN: string val latex_body: string -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
@@ -584,6 +586,8 @@
 val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN;
 val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN;
 val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN;
+val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN;
+val (latex_bodyN, latex_body) = markup_string "latex_body" kindN;
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 

--- a/src/Pure/PIDE/markup.scala	Sat Nov 20 13:53:34 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Nov 20 18:15:09 2021 +0100
@@ -375,6 +375,8 @@
   val Latex_Macro0 = new Markup_String("latex_macro0", NAME)
   val Latex_Macro = new Markup_String("latex_macro", NAME)
   val Latex_Environment = new Markup_String("latex_environment", NAME)
+  val Latex_Heading = new Markup_String("latex_heading", KIND)
+  val Latex_Body = new Markup_String("latex_body", KIND)
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 

--- a/src/Pure/Thy/document_output.ML	Sat Nov 20 13:53:34 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Sat Nov 20 18:15:09 2021 +0100
@@ -200,11 +200,10 @@
   (case tok of
     Ignore => []
   | Token tok => output_token ctxt tok
-  | Heading (cmd, source) =>
-      XML.enclose ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
-        (output_document ctxt {markdown = false} source)
-  | Body (cmd, source) =>
-      Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)
+  | Heading (kind, source) =>
+      [XML.Elem (Markup.latex_heading kind, output_document ctxt {markdown = false} source)]
+  | Body (kind, source) =>
+      [XML.Elem (Markup.latex_body kind, output_document ctxt {markdown = true} source)]
   | Raw source =>
       Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n");
 

--- a/src/Pure/Thy/latex.scala	Sat Nov 20 13:53:34 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Nov 20 18:15:09 2021 +0100
@@ -86,6 +86,12 @@
     def latex_environment(name: String, body: Text): Text =
       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)
+
+    def latex_body(kind: String, body: Text): Text =
+      latex_environment("isamarkup" + kind, body)
+
     def index_item(item: Index_Item.Value): String =
     {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
@@ -129,6 +135,10 @@
             traverse(latex_macro(name, body))
           case XML.Elem(Markup.Latex_Environment(name), body) =>
             traverse(latex_environment(name, body))
+          case XML.Elem(Markup.Latex_Heading(kind), body) =>
+            traverse(latex_heading(kind, body))
+          case XML.Elem(Markup.Latex_Body(kind), body) =>
+            traverse(latex_body(kind, body))
           case Index_Entry(entry) =>
             traverse(index_entry(entry))
           case t: XML.Tree =>