# HG changeset patch
# User wenzelm
# Date 1719526534 -7200
# Node ID 2c07b9b2f9f48c593e2e1a016bc1d12a54da81fb
# Parent  6e865cd2234982a49fe44e0566324b02502485ed
minor performance tuning: more direct Bytes with Symbol.encode;

diff -r 6e865cd22349 -r 2c07b9b2f9f4 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -657,7 +657,7 @@
   def uncompress_errors(bytes: Bytes, cache: XML.Cache = XML.Cache.make()): List[String] =
     if (bytes.is_empty) Nil
     else {
-      XML.Decode.list(YXML.string_of_body)(
+      XML.Decode.list(YXML.string_of_body(_))(
         YXML.parse_body(bytes.uncompress(cache = cache.compress).text, cache = cache))
     }
 
diff -r 6e865cd22349 -r 2c07b9b2f9f4 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -294,7 +294,7 @@
                     val args =
                       Protocol.Export.Args(
                         theory_name = theory_name, name = name, compress = compress)
-                    val body = Bytes(Symbol.encode(YXML.string_of_body(xml)))
+                    val body = YXML.bytes_of_body(xml, recode = Symbol.encode)
                     export_consumer.make_entry(session_name, args, body)
                   }
                 }
diff -r 6e865cd22349 -r 2c07b9b2f9f4 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -533,7 +533,8 @@
   def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
     YXML.parse_body_failsafe(decode(text), cache = cache)
 
-  def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
+  def encode_yxml(body: XML.Body): String =
+    YXML.string_of_body(body, recode = encode)
 
   def decode_strict(text: String): String = {
     val decoded = decode(text)
diff -r 6e865cd22349 -r 2c07b9b2f9f4 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -60,26 +60,28 @@
     }
   }
 
-  class Output_String(builder: StringBuilder) extends Output {
+  class Output_String(builder: StringBuilder, recode: String => String = identity) extends Output {
     override def byte(b: Byte): Unit = { builder += b.toChar }
-    override def string(s: String): Unit = { builder ++= s }
+    override def string(s: String): Unit = { builder ++= recode(s) }
     def result(ts: List[XML.Tree]): String = { traverse(ts); builder.toString }
   }
 
-  class Output_Bytes(builder: Bytes.Builder) extends Output {
+  class Output_Bytes(builder: Bytes.Builder, recode: String => String = identity) extends Output {
     override def byte(b: Byte): Unit = { builder += b }
-    override def string(s: String): Unit = { builder += s }
+    override def string(s: String): Unit = { builder += recode(s) }
   }
 
-  def string_of_body(body: XML.Body): String =
-    new Output_String(new StringBuilder).result(body)
+  def string_of_body(body: XML.Body, recode: String => String = identity): String =
+    new Output_String(new StringBuilder, recode = recode).result(body)
 
-  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+  def string_of_tree(tree: XML.Tree, recode: String => String = identity): String =
+    string_of_body(List(tree), recode = recode)
 
-  def bytes_of_body(body: XML.Body): Bytes =
-    Bytes.Builder.use()(builder => new Output_Bytes(builder).traverse(body))
+  def bytes_of_body(body: XML.Body, recode: String => String = identity): Bytes =
+    Bytes.Builder.use()(builder => new Output_Bytes(builder, recode = recode).traverse(body))
 
-  def bytes_of_tree(tree: XML.Tree): Bytes = bytes_of_body(List(tree))
+  def bytes_of_tree(tree: XML.Tree, recode: String => String = identity): Bytes =
+    bytes_of_body(List(tree), recode = recode)
 
 
   /* parsing */
diff -r 6e865cd22349 -r 2c07b9b2f9f4 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Jun 27 23:53:31 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Jun 28 00:15:34 2024 +0200
@@ -33,7 +33,7 @@
       write(file_name, Bytes(text))
 
     def write(file_name: Path, body: XML.Body): Unit =
-      write(file_name, Symbol.encode(YXML.string_of_body(body)))
+      write(file_name, YXML.bytes_of_body(body, recode = Symbol.encode))
   }
 
   sealed case class Aspect(