more symbolic latex_output via XML (using YXML within text);

--- a/src/Pure/PIDE/markup.ML	Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 20 20:42:41 2021 +0100
@@ -157,6 +157,8 @@
   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 latex_delimN: string val latex_delim: string -> T
+  val latex_tagN: string val latex_tag: 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
@@ -590,6 +592,8 @@
 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;
+val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN;
+val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN;
 
 
 (* Markdown document structure *)

--- a/src/Pure/PIDE/markup.scala	Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Nov 20 20:42:41 2021 +0100
@@ -377,6 +377,9 @@
   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_Delim = new Markup_String("latex_delim", NAME)
+  val Latex_Tag = new Markup_String("latex_tag", NAME)
+
   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 19:39:22 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Sat Nov 20 20:42:41 2021 +0100
@@ -241,10 +241,15 @@
   if x = y then I
   else (case which (x, y) of NONE => I | SOME txt => fold cons (Latex.string (f txt)));
 
-val begin_tag = edge #2 Latex.begin_tag;
-val end_tag = edge #1 Latex.end_tag;
-fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
-fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
+val markup_tag = YXML.output_markup o Markup.latex_tag;
+val markup_delim = YXML.output_markup o Markup.latex_delim;
+val bg_delim = #1 o markup_delim;
+val en_delim = #2 o markup_delim;
+
+val begin_tag = edge #2 (#1 o markup_tag);
+val end_tag = edge #1 (#2 o markup_tag);
+fun open_delim delim e = edge #2 bg_delim e #> delim #> edge #2 en_delim e;
+fun close_delim delim e = edge #1 bg_delim e #> delim #> edge #1 en_delim e;
 
 fun document_tag cmd_pos state state' tagging_stack =
   let

--- a/src/Pure/Thy/latex.ML	Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Nov 20 20:42:41 2021 +0100
@@ -22,10 +22,6 @@
   val output_syms: string -> string
   val symbols: Symbol_Pos.T list -> text
   val symbols_output: Symbol_Pos.T list -> text
-  val begin_delim: string -> string
-  val end_delim: string -> string
-  val begin_tag: string -> string
-  val end_tag: string -> string
   val environment_text: string -> text -> text
   val isabelle_body: string -> text -> text
   val theory_entry: string -> string
@@ -196,14 +192,6 @@
   text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
 
 
-(* tags *)
-
-val begin_delim = enclose_name "%\n\\isadelim" "\n";
-val end_delim = enclose_name "%\n\\endisadelim" "\n";
-val begin_tag = enclose_name "%\n\\isatag" "\n";
-fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose_name "{\\isafold" "}%\n" tg;
-
-
 (* theory presentation *)
 
 fun environment_text name =

--- a/src/Pure/Thy/latex.scala	Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Nov 20 20:42:41 2021 +0100
@@ -16,6 +16,36 @@
 
 object Latex
 {
+  /* output name for LaTeX macros */
+
+  private val output_name_map: Map[Char, String] =
+    Map('_' -> "UNDERSCORE",
+      '\'' -> "PRIME",
+      '0' -> "ZERO",
+      '1' -> "ONE",
+      '2' -> "TWO",
+      '3' -> "THREE",
+      '4' -> "FOUR",
+      '5' -> "FIVE",
+      '6' -> "SIX",
+      '7' -> "SEVEN",
+      '8' -> "EIGHT",
+      '9' -> "NINE")
+
+  def output_name(name: String): String =
+    if (name.exists(output_name_map.keySet)) {
+      val res = new StringBuilder
+      for (c <- name) {
+        output_name_map.get(c) match {
+          case None => res += c
+          case Some(s) => res ++= s
+        }
+      }
+      res.toString
+    }
+    else name
+
+
   /* index entries */
 
   def index_escape(str: String): String =
@@ -92,6 +122,18 @@
     def latex_body(kind: String, body: Text): Text =
       latex_environment("isamarkup" + kind, body)
 
+    def latex_delim(name: String, body: Text): Text =
+    {
+      val s = output_name(name)
+      XML.enclose("%\n\\isadelim" + s + "\n", "%\n\\endisadelim" + s + "\n", body)
+    }
+
+    def latex_tag(name: String, body: Text): Text =
+    {
+      val s = output_name(name)
+      XML.enclose("%\n\\isatag" + s + "\n", "%\n\\endisatag" + s + "\n{\\isafold" + s + "}%\n", body)
+    }
+
     def index_item(item: Index_Item.Value): String =
     {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
@@ -139,6 +181,10 @@
             traverse(latex_heading(kind, body))
           case XML.Elem(Markup.Latex_Body(kind), body) =>
             traverse(latex_body(kind, body))
+          case XML.Elem(Markup.Latex_Delim(name), body) =>
+            traverse(latex_delim(name, body))
+          case XML.Elem(Markup.Latex_Tag(name), body) =>
+            traverse(latex_tag(name, body))
           case Index_Entry(entry) =>
             traverse(index_entry(entry))
           case t: XML.Tree =>