clarified signature: more explicit types;

--- a/src/Pure/General/html.scala	Thu Jun 27 00:11:53 2024 +0200
+++ b/src/Pure/General/html.scala	Thu Jun 27 22:09:09 2024 +0200
@@ -170,8 +170,10 @@
     hidden: Boolean,
     permissive: Boolean
   ): Unit = {
+    val xml_output = new XML.Output(s)
+
     def output_string(str: String): Unit =
-      XML.output_string(s, str, permissive = permissive)
+      xml_output.string(str, permissive = permissive)
 
     def output_hidden(body: => Unit): Unit =
       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
@@ -181,11 +183,11 @@
         control_block_begin.get(sym) match {
           case Some(op) if control_blocks =>
             output_hidden(output_string(sym))
-            XML.output_elem(s, Markup(op.name, Nil))
+            xml_output.elem(Markup(op.name, Nil))
           case _ =>
             control_block_end.get(sym) match {
               case Some(op) if control_blocks =>
-                XML.output_elem_end(s, op.name)
+                xml_output.end_elem(op.name)
                 output_hidden(output_string(sym))
               case _ =>
                 if (hidden && Symbol.is_control_encoded(sym)) {
@@ -207,9 +209,9 @@
         control.get(ctrl) match {
           case Some(op) if Symbol.is_controllable(sym) =>
             output_hidden(output_symbol(ctrl))
-            XML.output_elem(s, Markup(op.name, Nil))
+            xml_output.elem(Markup(op.name, Nil))
             output_symbol(sym)
-            XML.output_elem_end(s, op.name)
+            xml_output.end_elem(op.name)
           case _ =>
             output_symbol(ctrl)
             output_symbol(sym)
@@ -234,18 +236,20 @@
       "ul", "ol", "dl", "li", "dt", "dd")
 
   def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit = {
+    val xml_output = new XML.Output(s)
+
     def output_body(body: XML.Body): Unit = {
       val control_blocks = check_control_blocks(body)
       body foreach {
         case XML.Elem(markup, Nil) =>
-          XML.output_elem(s, markup, end = true)
+          xml_output.elem(markup, end = true)
         case XML.Elem(Markup(Markup.RAW_HTML, _), body) =>
           XML.traverse_text(body)(()) { case (_, raw) => s.append(raw) }
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
-          XML.output_elem(s, markup)
+          xml_output.elem(markup)
           output_body(ts)
-          XML.output_elem_end(s, markup.name)
+          xml_output.end_elem(markup.name)
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
           output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true)

--- a/src/Pure/PIDE/xml.scala	Thu Jun 27 00:11:53 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 27 22:09:09 2024 +0200
@@ -46,6 +46,20 @@
   def enclose(bg: String, en:String, body: Body): Body =
     string(bg) ::: body ::: string(en)
 
+  trait Traversal {
+    def text(s: String): Unit
+    def elem(markup: Markup, end: Boolean = false): Unit
+    def end_elem(name: String): Unit
+
+    def tree(t: Tree): Unit =
+      t match {
+        case Text(s) => text(s)
+        case Elem(markup, Nil) => elem(markup, end = true)
+        case Elem(markup, ts) => elem(markup); trees(ts); end_elem(markup.name)
+      }
+    def trees(ts: Iterable[Tree]): Unit = ts.foreach(tree)
+  }
+
 
   /* name space */
 
@@ -125,66 +139,61 @@
 
   val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
 
-  def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = {
-    c match {
-      case '<' => s ++= "&lt;"
-      case '>' => s ++= "&gt;"
-      case '&' => s ++= "&amp;"
-      case '"' if !permissive => s ++= "&quot;"
-      case '\'' if !permissive => s ++= "&apos;"
-      case _ => s += c
+  class Output(builder: StringBuilder) extends Traversal {
+    def string(str: String, permissive: Boolean = false): Unit = {
+      if (str == null) { builder ++= str }
+      else {
+        for (c <- str) {
+          c match {
+            case '<' => builder ++= "&lt;"
+            case '>' => builder ++= "&gt;"
+            case '&' => builder ++= "&amp;"
+            case '"' if !permissive => builder ++= "&quot;"
+            case '\'' if !permissive => builder ++= "&apos;"
+            case _ => builder += c
+          }
+        }
+      }
     }
-  }
+
+    override def text(str: String): Unit = string(str)
 
-  def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = {
-    if (str == null) s ++= str
-    else str.iterator.foreach(output_char(s, _, permissive = permissive))
+    override def elem(markup: Markup, end: Boolean = false): Unit = {
+      builder += '<'
+      builder ++= markup.name
+      for ((a, b) <- markup.properties) {
+        builder += ' '
+        builder ++= a
+        builder += '='
+        builder += '"'
+        string(b)
+        builder += '"'
+      }
+      if (end) builder += '/'
+      builder += '>'
+    }
+
+    def end_elem(name: String): Unit = {
+      builder += '<'
+      builder += '/'
+      builder ++= name
+      builder += '>'
+    }
+
+    def result(ts: Iterable[Tree]): String = { trees(ts); builder.toString }
+    def result(t: Tree): String = { tree(t); builder.toString }
   }
 
-  def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = {
-    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): Unit = {
-    s += '<'
-    s += '/'
-    s ++= name
-    s += '>'
-  }
-
-  def string_of_body(body: Body): String = {
-    val s = new StringBuilder
-
-    def tree(t: Tree): Unit =
-      t match {
-        case XML.Elem(markup, Nil) =>
-          output_elem(s, markup, end = true)
-        case XML.Elem(markup, ts) =>
-          output_elem(s, markup)
-          ts.foreach(tree)
-          output_elem_end(s, markup.name)
-        case XML.Text(txt) => output_string(s, txt)
-      }
-    body.foreach(tree)
-    s.toString
-  }
+  def string_of_body(body: Body): String =
+    if (body.isEmpty) ""
+    else new Output(new StringBuilder).result(body)
 
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
   def text(s: String): String = string_of_tree(XML.Text(s))
 
 
+
   /** cache **/
 
   object Cache {