clarified signature: no symbol markup within XML attributes;

--- a/src/Pure/PIDE/xml.scala	Sat Jan 30 17:15:14 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 30 18:34:37 2021 +0100
@@ -146,27 +146,43 @@
     else str.iterator.foreach(output_char(s, _, permissive = permissive))
   }
 
+  def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false)
+  {
+    s += '<'
+    s ++= markup.name
+    for ((a, b) <- markup.properties) {
+      s += ' '
+      s ++= a
+      s += '='
+      s += '"'
+      output_string(s, b)
+      s += '"'
+    }
+    if (end) s += '/'
+    s += '>'
+  }
+
+  def output_elem_end(s: StringBuilder, name: String)
+  {
+    s += '<'
+    s += '/'
+    s ++= name
+    s += '>'
+  }
+
   def string_of_body(body: Body): String =
   {
     val s = new StringBuilder
 
-    def text(txt: String) { output_string(s, txt) }
-    def elem(markup: Markup)
-    {
-      s ++= markup.name
-      for ((a, b) <- markup.properties) {
-        s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"'
-      }
-    }
     def tree(t: Tree): Unit =
       t match {
         case XML.Elem(markup, Nil) =>
-          s += '<'; elem(markup); s ++= "/>"
+          output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
-          s += '<'; elem(markup); s += '>'
+          output_elem(s, markup)
           ts.foreach(tree)
-          s ++= "</"; s ++= markup.name; s += '>'
-        case XML.Text(txt) => text(txt)
+          output_elem_end(s, markup.name)
+        case XML.Text(txt) => output_string(s, txt)
       }
     body.foreach(tree)
     s.toString

--- a/src/Pure/Thy/html.scala	Sat Jan 30 17:15:14 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 18:34:37 2021 +0100
@@ -28,11 +28,8 @@
 
   def output(s: StringBuilder, text: String, hidden: Boolean, permissive: Boolean)
   {
-    def output_char(c: Char): Unit =
-      XML.output_char(s, c, permissive = permissive)
-
     def output_string(str: String): Unit =
-      str.iterator.foreach(output_char)
+      XML.output_string(s, str, permissive = permissive)
 
     def output_hidden(body: => Unit): Unit =
       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
@@ -63,9 +60,9 @@
         control.get(ctrl) match {
           case Some(elem) if Symbol.is_controllable(sym) =>
             output_hidden(output_symbol(ctrl))
-            s += '<'; s ++= elem; s += '>'
+            XML.output_elem(s, Markup(elem, Nil))
             output_symbol(sym)
-            s ++= "</"; s ++= elem; s += '>'
+            XML.output_elem_end(s, elem)
           case _ =>
             output_symbol(ctrl)
             output_symbol(sym)
@@ -88,27 +85,15 @@
 
   def output(s: StringBuilder, body: XML.Body, hidden: Boolean, structural: Boolean)
   {
-    def elem(markup: Markup)
-    {
-      s ++= markup.name
-      for ((a, b) <- markup.properties) {
-        s += ' '
-        s ++= a
-        s += '='
-        s += '"'
-        output(s, b, hidden = hidden, permissive = false)
-        s += '"'
-      }
-    }
     def tree(t: XML.Tree): Unit =
       t match {
         case XML.Elem(markup, Nil) =>
-          s += '<'; elem(markup); s ++= "/>"
+          XML.output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
-          s += '<'; elem(markup); s += '>'
+          XML.output_elem(s, markup)
           ts.foreach(tree)
-          s ++= "</"; s ++= markup.name; s += '>'
+          XML.output_elem_end(s, markup.name)
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
           output(s, txt, hidden = hidden, permissive = true)