clarified signature;

--- a/src/Pure/PIDE/yxml.scala	Tue Jun 25 18:09:53 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Jun 26 15:22:20 2024 +0200
@@ -14,8 +14,11 @@
 object YXML {
   /* chunk markers */
 
-  val X = '\u0005'
-  val Y = '\u0006'
+  val X_byte: Byte = 5
+  val Y_byte: Byte = 6
+
+  val X = X_byte.toChar
+  val Y = Y_byte.toChar
 
   val is_X: Char => Boolean = _ == X
   val is_Y: Char => Boolean = _ == Y
@@ -31,31 +34,46 @@
 
   /* string representation */
 
-  def traversal(string: String => Unit, body: XML.Body): Unit = {
+  trait Output {
+    def byte(b: Byte): Unit
+    def string(s: String): Unit
     def tree(t: XML.Tree): Unit =
       t match {
         case XML.Elem(markup @ Markup(name, atts), ts) =>
           if (markup.is_empty) ts.foreach(tree)
           else {
-            string(XY_string)
+            byte(X_byte)
+            byte(Y_byte)
             string(name)
-            for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
-            string(X_string)
+            for ((a, b) <- atts) {
+              byte(Y_byte)
+              string(a)
+              byte('='.toByte)
+              string(b)
+            }
+            byte(X_byte)
             ts.foreach(tree)
-            string(XYX_string)
+            byte(X_byte)
+            byte(Y_byte)
+            byte(X_byte)
           }
         case XML.Text(text) => string(text)
       }
-    body.foreach(tree)
+    def trees(ts: Iterable[XML.Tree]): Unit = ts.foreach(tree)
   }
 
-  def string_of_body(body: XML.Body): String = {
-    val s = new StringBuilder
-    traversal(str => s ++= str, body)
-    s.toString
+  class Output_String(builder: StringBuilder) extends Output {
+    override def byte(b: Byte): Unit = { builder += b.toChar }
+    override def string(s: String): Unit = { builder ++= s }
+    def result(ts: Iterable[XML.Tree]): String = { trees(ts); builder.toString }
+    def result(t: XML.Tree): String = { tree(t); builder.toString }
   }
 
-  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+  def string_of_body(body: XML.Body): String =
+    new Output_String(new StringBuilder).result(body)
+
+  def string_of_tree(tree: XML.Tree): String =
+    new Output_String(new StringBuilder).result(tree)
 
 
   /* parsing */

--- a/src/Pure/Tools/dump.scala	Tue Jun 25 18:09:53 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Wed Jun 26 15:22:20 2024 +0200
@@ -33,8 +33,7 @@
       write(file_name, Bytes(text))
 
     def write(file_name: Path, body: XML.Body): Unit =
-      using(File.writer(write_path(file_name).file))(
-        writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
+      write(file_name, Symbol.encode(YXML.string_of_body(body)))
   }
 
   sealed case class Aspect(