more symbolic latex output;
discontinued Latex.output_text, which is in conflict with symbolic output;

--- a/src/Pure/PIDE/markup.ML	Sun Nov 14 20:15:28 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Nov 14 20:40:41 2021 +0100
@@ -150,6 +150,8 @@
   val document_tagN: string val document_tag: string -> T
   val document_latexN: string val document_latex: T
   val latex_outputN: string val latex_output: 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
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
@@ -576,6 +578,8 @@
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
 val (latex_outputN, latex_output) = markup_elem "latex_output";
+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;
 
 
 (* Markdown document structure *)

--- a/src/Pure/PIDE/markup.scala	Sun Nov 14 20:15:28 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Nov 14 20:40:41 2021 +0100
@@ -372,6 +372,8 @@
   val Document_Latex = new Markup_Elem("document_latex")
 
   val Latex_Output = new Markup_Elem("latex_output")
+  val Latex_Index_Item = new Markup_Elem("latex_index_item")
+  val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 
 
   /* Markdown document structure */

--- a/src/Pure/Thy/latex.ML	Sun Nov 14 20:15:28 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 14 20:40:41 2021 +0100
@@ -12,7 +12,6 @@
   val block: text -> XML.tree
   val output: text -> text
   val enclose_text: string -> string -> text -> text
-  val output_text: text -> string
   val output_name: string -> string
   val output_ascii: string -> string
   val output_ascii_breakable: string -> string -> string
@@ -27,7 +26,6 @@
   val environment_text: string -> text -> text
   val isabelle_body: string -> text -> text
   val theory_entry: string -> string
-  val index_escape: string -> string
   type index_item = {text: text, like: string}
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
@@ -56,16 +54,6 @@
 
 fun output body = [XML.Elem (Markup.latex_output, body)];
 
-val output_text =
-  let
-    fun document_latex text =
-      text |> maps
-        (fn XML.Elem ((name, _), body) =>
-              if name = Markup.document_latexN orelse name = Markup.latex_outputN
-              then document_latex body else []
-          | t => [t])
-  in XML.content_of o document_latex end;
-
 fun enclose_text bg en body = string bg @ body @ string en;
 
 
@@ -229,24 +217,12 @@
 type index_item = {text: text, like: string};
 type index_entry = {items: index_item list, def: bool};
 
-val index_escape =
-  translate_string (fn s =>
-    if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
-    else if member_string "\\{}#" s then "\"" ^ s else s);
-
 fun index_item (item: index_item) =
-  let
-    val like_text =
-      if #like item = "" then ""
-      else index_escape (#like item) ^ "@";
-    val item_text = index_escape (output_text (#text item));
-  in like_text ^ item_text end;
+  XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
 
 fun index_entry (entry: index_entry) =
-  (space_implode "!" (map index_item (#items entry)) ^
-    "|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))
-  |> enclose "\\index{" "}"
-  |> string;
+  [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
+    map index_item (#items entry))];
 
 fun index_binding NONE = I
   | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));

--- a/src/Pure/Thy/latex.scala	Sun Nov 14 20:15:28 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Sun Nov 14 20:40:41 2021 +0100
@@ -16,6 +16,53 @@
 
 object Latex
 {
+  /* index entries */
+
+  def index_escape(str: String): String =
+  {
+    val special1 = "!\"@|"
+    val special2 = "\\{}#"
+    if (str.exists(c => special1.contains(c) || special2.contains(c))) {
+      val res = new StringBuilder
+      for (c <- str) {
+        if (special1.contains(c)) {
+          res ++= "\\char"
+          res ++= Value.Int(c)
+        }
+        else {
+          if (special2.contains(c)) { res += '"'}
+          res += c
+        }
+      }
+      res.toString
+    }
+    else str
+  }
+
+  object Index_Item
+  {
+    sealed case class Value(text: Text, like: String)
+    def unapply(tree: XML.Tree): Option[Value] =
+      tree match {
+        case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) =>
+          Some(Value(text, XML.content(like)))
+        case _ => None
+      }
+  }
+
+  object Index_Entry
+  {
+    sealed case class Value(items: List[Index_Item.Value], kind: String)
+    def unapply(tree: XML.Tree): Option[Value] =
+      tree match {
+        case XML.Elem(Markup.Latex_Index_Entry(kind), body) =>
+          val items = body.map(Index_Item.unapply)
+          if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None
+        case _ => None
+      }
+  }
+
+
   /* output text and positions */
 
   type Text = XML.Body
@@ -28,7 +75,27 @@
 
   class Output
   {
-    def latex_output(latex_text: Text): Text = List(XML.Text(apply(latex_text)))
+    def latex_output(latex_text: Text): String = apply(latex_text)
+
+    def latex_macro(name: String, arg: Text): Text =
+      XML.string("\\" + name + "{") ::: arg ::: XML.string("}")
+
+    def index_item(item: Index_Item.Value): String =
+    {
+      val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
+      val text = index_escape(latex_output(item.text))
+      like + text
+    }
+
+    def index_entry(entry: Index_Entry.Value): Text =
+    {
+      val items = entry.items.map(index_item).mkString("!")
+      val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind)
+      latex_macro("index", XML.string(items + kind))
+    }
+
+
+    /* standard output of text with per-line positions */
 
     def apply(latex_text: Text, file_pos: String = ""): String =
     {
@@ -42,14 +109,16 @@
           case XML.Text(s) =>
             line += s.count(_ == '\n')
             result += s
-          case XML.Elem(Markup.Latex_Output(_), body) =>
-            traverse(latex_output(body))
           case XML.Elem(Markup.Document_Latex(props), body) =>
             for { l <- Position.Line.unapply(props) if positions.nonEmpty } {
               val s = position(Value.Int(line), Value.Int(l))
               if (positions.last != s) positions += s
             }
             traverse(body)
+          case XML.Elem(Markup.Latex_Output(_), body) =>
+            traverse(XML.string(latex_output(body)))
+          case Index_Entry(entry) =>
+            traverse(index_entry(entry))
           case _: XML.Elem =>
         }
       }