# HG changeset patch
# User wenzelm
# Date 1719601317 -7200
# Node ID cba532bf431627dd4356c2b1907b9c6b7c926528
# Parent  6ed82923d51df96d4022b8b544cae7dfe9a2f130# Parent  acbd22e7e3ecf9c6c75eb54695340587ef7d5a40
merged

diff -r 6ed82923d51d -r cba532bf4316 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -650,14 +650,14 @@
   ): Option[Bytes] =
     if (errors.isEmpty) None
     else {
-      Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
+      Some(YXML.bytes_of_body(XML.Encode.list(XML.Encode.string)(errors)).
         compress(cache = cache))
     }
 
   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 6ed82923d51d -r cba532bf4316 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/build.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -714,13 +714,12 @@
     theory_context: Export.Theory_Context,
     unicode_symbols: Boolean = false
   ): Option[Document.Snapshot] = {
-    def decode_bytes(bytes: Bytes): String =
-      Symbol.output(unicode_symbols, bytes.text)
+    def decode(str: String): String = Symbol.output(unicode_symbols, str)
 
     def read(name: String): Export.Entry = theory_context(name, permissive = true)
 
     def read_xml(name: String): XML.Body =
-      YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache)
+      YXML.parse_body(read(name).bytes.text, recode = decode, cache = theory_context.cache)
 
     def read_source_file(name: String): Store.Source_File =
       theory_context.session_context.source_file(name)
@@ -741,14 +740,14 @@
 
           val file = read_source_file(name)
           val bytes = file.bytes
-          val text = decode_bytes(bytes)
+          val text = decode(bytes.text)
           val chunk = Symbol.Text_Chunk(text)
 
           Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
             Document.Blobs.Item(bytes, text, chunk, changed = false)
         }
 
-      val thy_source = decode_bytes(read_source_file(thy_file).bytes)
+      val thy_source = decode(read_source_file(thy_file).bytes.text)
       val thy_xml = read_xml(Export.MARKUP)
       val blobs_xml =
         for (i <- (1 to blobs.length).toList)
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Fri Jun 28 21:01:57 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 6ed82923d51d -r cba532bf4316 src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/export.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -194,7 +194,8 @@
 
     def text: String = bytes.text
 
-    def yxml: XML.Body = YXML.parse_body(bytes.text, cache = cache)
+    def yxml(recode: String => String = identity): XML.Body =
+      YXML.parse_body(bytes.text, recode = recode, cache = cache)
   }
 
   def make_regex(pattern: String): Regex = {
@@ -536,9 +537,9 @@
     def apply(name: String, permissive: Boolean = false): Entry =
       session_context.apply(theory, name, permissive = permissive)
 
-    def yxml(name: String): XML.Body =
+    def yxml(name: String, recode: String => String = identity): XML.Body =
       get(name) match {
-        case Some(entry) => entry.yxml
+        case Some(entry) => entry.yxml(recode = recode)
         case None => Nil
       }
 
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/Build/export_theory.scala
--- a/src/Pure/Build/export_theory.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Build/export_theory.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -391,7 +391,7 @@
 
     for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
     yield {
-      val body = entry.yxml
+      val body = entry.yxml()
       val (typargs, (args, (prop_body, proof_body))) = {
         import XML.Decode._
         import Term_XML.Decode._
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -17,6 +17,7 @@
 import com.github.luben.zstd
 
 import scala.collection.mutable.ArrayBuffer
+import scala.collection.mutable
 
 
 object Bytes {
@@ -168,70 +169,86 @@
   }
 
   final class Builder private[Bytes](hint: Long) {
-    private var size = 0L
     private var chunks =
       new ArrayBuffer[Array[Byte]](if (hint <= 0) 16 else (hint / chunk_size).toInt)
+
+    private var buffer_list: mutable.ListBuffer[Array[Byte]] = null
     private var buffer =
-      new ByteArrayOutputStream(if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt)
+      new Array[Byte](if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt)
+    private var buffer_index = 0
+    private var buffer_total = 0
 
-    private def buffer_free(): Int = chunk_size.toInt - buffer.size()
-    private def buffer_check(): Unit =
-      if (buffer_free() == 0) {
-        chunks += buffer.toByteArray
-        buffer = new ByteArrayOutputStream(chunk_size.toInt)
+    private def buffer_content(): Array[Byte] =
+      if (buffer_list != null) {
+        val array = new Array[Byte](buffer_total)
+        var i = 0
+        for (b <- buffer_list) {
+          val n = b.length
+          System.arraycopy(b, 0, array, i, n)
+          i += n
+        }
+        System.arraycopy(buffer, 0, array, i, buffer_index)
+        array
+      }
+      else if (buffer_index == buffer.length) buffer else Arrays.copyOf(buffer, buffer_index)
+
+    private def buffer_check(request: Int = 0): Unit =
+      if (buffer_index == buffer.length) {
+        if (buffer_total == chunk_size) {
+          chunks += buffer_content()
+          buffer_list = null
+          buffer = new Array[Byte](chunk_size.toInt)
+          buffer_total = 0
+          buffer_index = 0
+        }
+        else {
+          if (buffer_list == null) { buffer_list = new mutable.ListBuffer }
+          buffer_list += buffer
+          buffer_index = 0
+          val limit = (chunk_size - buffer_total).toInt
+          buffer = new Array[Byte]((buffer_total max request) min limit)
+        }
       }
 
     def += (b: Byte): Unit = {
-      size += 1
-      buffer.write(b)
+      buffer(buffer_index) = b
+      buffer_total += 1
+      buffer_index += 1
       buffer_check()
     }
 
-    def += (s: CharSequence): Unit = {
-      val n = s.length
-      if (n > 0) {
-        if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) }
-        else {
-          var i = 0
-          while (i < n) {
-            buffer.write(s.charAt(i).toByte)
-            size += 1
-            i += 1
-            buffer_check()
-          }
-        }
-      }
-    }
-
     def += (array: Array[Byte], offset: Int, length: Int): Unit = {
       if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {
         throw new IndexOutOfBoundsException
       }
-      else if (length > 0) {
+      else {
         var i = offset
         var n = length
         while (n > 0) {
-          val m = buffer_free()
-          if (m > 0) {
-            val l = m min n
-            buffer.write(array, i, l)
-            size += l
-            i += l
-            n -= l
-          }
-          buffer_check()
+          val l = n min (buffer.length - buffer_index)
+          System.arraycopy(array, i, buffer, buffer_index, l)
+          buffer_total += l
+          buffer_index += l
+          i += l
+          n -= l
+          buffer_check(request = n)
         }
       }
     }
 
+    def += (s: CharSequence): Unit =
+      if (s.length > 0) { this += UTF8.bytes(s.toString) }
+
     def += (array: Array[Byte]): Unit = { this += (array, 0, array.length) }
 
     def += (a: Subarray): Unit = { this += (a.array, a.offset, a.length) }
 
     private def done(): Bytes = {
       val cs = chunks.toArray
-      val b = buffer.toByteArray
+      val b = buffer_content()
+      val size = cs.foldLeft(b.length.toLong)({ case (n, a) => n + a.length })
       chunks = null
+      buffer_list = null
       buffer = null
       new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, size)
     }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/file.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -205,13 +205,12 @@
   def read(path: Path): String = read(path.file)
 
 
-  def read_stream(reader: BufferedReader): String = {
-    val output = new StringBuilder(100)
-    var c = -1
-    while ({ c = reader.read; c != -1 }) output += c.toChar
-    reader.close()
-    output.toString
-  }
+  def read_stream(reader: BufferedReader): String =
+    Library.string_builder(hint = 100) { output =>
+      var c = -1
+      while ({ c = reader.read; c != -1 }) output += c.toChar
+      reader.close()
+    }
 
   def read_stream(stream: InputStream): String =
     read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/html.scala
--- a/src/Pure/General/html.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/html.scala	Fri Jun 28 21:01:57 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)
@@ -222,8 +224,9 @@
 
   def output(text: String): String = {
     val control_blocks = check_control_blocks(List(XML.Text(text)))
-    Library.make_string(output(_, text,
-      control_blocks = control_blocks, hidden = false, permissive = true))
+    Library.string_builder() { builder =>
+      output(builder, text, control_blocks = control_blocks, hidden = false, permissive = true)
+    }
   }
 
 
@@ -234,18 +237,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) }
+          XML.traverse_text(body, (), (_, 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)
@@ -255,7 +260,9 @@
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
-    Library.make_string(output(_, body, hidden, structural), capacity = XML.text_length(body) * 2)
+    Library.string_builder(hint = XML.text_length(body) * 2) { builder =>
+      output(builder, body, hidden, structural)
+    }
 
   def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
     output(List(tree), hidden, structural)
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/json.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -196,49 +196,44 @@
         case _ => false
       }
 
-    def apply(json: T): S = {
-      val result = new StringBuilder
-
-      def output(x: T): Unit = {
-        if (!output_atom(x, result)) {
-          x match {
-            case Object(obj) =>
-              result += '{'
-              Library.separate(None, obj.toList.map(Some(_))).foreach({
-                case None => result += ','
-                case Some((x, y)) =>
-                  output_string(x, result)
-                  result += ':'
-                  output(y)
-              })
-              result += '}'
-            case list: List[T] =>
-              result += '['
-              Library.separate(None, list.map(Some(_))).foreach({
-                case None => result += ','
-                case Some(x) => output(x)
-              })
-              result += ']'
-            case _ => error("Bad JSON value: " + x.toString)
+    def apply(json: T): S =
+      Library.string_builder() { result =>
+        def output(x: T): Unit = {
+          if (!output_atom(x, result)) {
+            x match {
+              case Object(obj) =>
+                result += '{'
+                Library.separate(None, obj.toList.map(Some(_))).foreach({
+                  case None => result += ','
+                  case Some((x, y)) =>
+                    output_string(x, result)
+                    result += ':'
+                    output(y)
+                })
+                result += '}'
+              case list: List[T] =>
+                result += '['
+                Library.separate(None, list.map(Some(_))).foreach({
+                  case None => result += ','
+                  case Some(x) => output(x)
+                })
+                result += ']'
+              case _ => error("Bad JSON value: " + x.toString)
+            }
           }
         }
+
+        output(json)
       }
 
-      output(json)
-      result.toString
-    }
-
     private def pretty_atom(x: T): Option[XML.Tree] = {
       val result = new StringBuilder
       val ok = output_atom(x, result)
       if (ok) Some(XML.Text(result.toString)) else None
     }
 
-    private def pretty_string(s: String): XML.Tree = {
-      val result = new StringBuilder
-      output_string(s, result)
-      XML.Text(result.toString)
-    }
+    private def pretty_string(s: String): XML.Tree =
+      XML.Text(Library.string_builder()(output_string(s, _)))
 
     private def pretty_tree(x: T): XML.Tree =
       x match {
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/latex.scala
--- a/src/Pure/General/latex.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/latex.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -34,14 +34,14 @@
 
   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
+      Library.string_builder() { res =>
+        for (c <- name) {
+          output_name_map.get(c) match {
+            case None => res += c
+            case Some(s) => res ++= s
+          }
         }
       }
-      res.toString
     }
     else name
 
@@ -52,18 +52,18 @@
     val special1 = "!\"@|"
     val special2 = "\\{}#"
     if (str.exists(c => special1.contains(c) || special2.contains(c))) {
-      val res = new StringBuilder
-      for (c <- str) {
-        if (special1.contains(c)) {
-          res ++= "\\char"
-          res ++= Value.Int(c)
-        }
-        else {
-          if (special2.contains(c)) { res += '"'}
-          res += c
+      Library.string_builder() { res =>
+        for (c <- str) {
+          if (special1.contains(c)) {
+            res ++= "\\char"
+            res ++= Value.Int(c)
+          }
+          else {
+            if (special2.contains(c)) { res += '"'}
+            res += c
+          }
         }
       }
-      res.toString
     }
     else str
   }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/properties.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -45,7 +45,7 @@
 
   def encode(ps: T): Bytes = {
     if (ps.isEmpty) Bytes.empty
-    else Bytes(YXML.string_of_body(XML.Encode.properties(ps)))
+    else YXML.bytes_of_body(XML.Encode.properties(ps))
   }
 
   def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
@@ -59,7 +59,7 @@
   ): Bytes = {
     if (ps.isEmpty) Bytes.empty
     else {
-      Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).
+      YXML.bytes_of_body(XML.Encode.list(XML.Encode.properties)(ps)).
         compress(options = options, cache = cache)
     }
   }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/scan.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -386,11 +386,10 @@
       if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
       else throw new IndexOutOfBoundsException
 
-    override def toString: String = {
-      val buf = new StringBuilder(length)
-      for (offset <- start until end) buf.append(seq(offset))
-      buf.toString
-    }
+    override def toString: String =
+      Library.string_builder(hint = length) { buf =>
+        for (offset <- start until end) buf.append(seq(offset))
+      }
   }
 
   abstract class Byte_Reader extends Reader[Char] with AutoCloseable
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/sql.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -29,18 +29,17 @@
 
   /* concrete syntax */
 
-  def string(s: String): Source = {
-    val q = '\''
-    val result = new StringBuilder(s.length + 10)
-    result += q
-    for (c <- s.iterator) {
-      if (c == '\u0000') error("Illegal NUL character in SQL string literal")
-      if (c == q) result += q
-      result += c
+  def string(s: String): Source =
+    Library.string_builder(hint = s.length + 10) { result =>
+      val q = '\''
+      result += q
+      for (c <- s.iterator) {
+        if (c == '\u0000') error("Illegal NUL character in SQL string literal")
+        if (c == q) result += q
+        result += c
+      }
+      result += q
     }
-    result += q
-    result.toString
-  }
 
   def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -70,12 +70,12 @@
     val special = "[]?*\\{} \"'"
     if (str.isEmpty) "\"\""
     else if (str.exists(special.contains)) {
-      val res = new StringBuilder
-      for (c <- str) {
-        if (special.contains(c)) res += '\\'
-        res += c
+      Library.string_builder() { res =>
+        for (c <- str) {
+          if (special.contains(c)) res += '\\'
+          res += c
+        }
       }
-      res.toString()
     }
     else str
   }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -265,20 +265,33 @@
       tab
     }
     def recode(text: String): String = {
-      val len = text.length
-      val matcher = new Symbol.Matcher(text)
-      val result = new StringBuilder(len)
-      var i = 0
-      while (i < len) {
-        val c = text(i)
-        if (min <= c && c <= max) {
-          val s = matcher.match_symbol(i)
-          result.append(table.getOrElse(s, s))
-          i += s.length
+      val n = text.length
+      val relevant = {
+        var i = 0
+        var found = false
+        while (i < n && !found) {
+          val c = text(i)
+          if (min <= c && c <= max) { found = true }
+          i += 1
         }
-        else { result.append(c); i += 1 }
+        found
       }
-      result.toString
+      if (relevant) {
+        val matcher = new Symbol.Matcher(text)
+        Library.string_builder(hint = n) { result =>
+          var i = 0
+          while (i < n) {
+            val c = text(i)
+            if (min <= c && c <= max) {
+              val s = matcher.match_symbol(i)
+              result.append(table.getOrElse(s, s))
+              i += s.length
+            }
+            else { result.append(c); i += 1 }
+          }
+        }
+      }
+      else text
     }
   }
 
@@ -528,20 +541,20 @@
   def encode(text: String): String = symbols.encode(text)
 
   def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
-    YXML.parse_body(decode(text), cache = cache)
+    YXML.parse_body(text, recode = decode, cache = cache)
 
   def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
-    YXML.parse_body_failsafe(decode(text), cache = cache)
+    YXML.parse_body_failsafe(text, recode = decode, 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)
     if (encode(decoded) == text) decoded
     else {
       val bad = new mutable.ListBuffer[Symbol]
-      for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
-        bad += s
+      for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s)) bad += s
       error("Bad Unicode symbols in text: " + commas_quote(bad))
     }
   }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/toml.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -614,94 +614,90 @@
 
     private def keys(ks: List[Key]): Str = ks.map(key).mkString(".")
 
-    private def inline(t: T, indent: Int = 0): Str = {
-      val result = new StringBuilder
-
-      result ++= Symbol.spaces(indent * 2)
-      (t: @unchecked) match {
-        case s: String =>
-          if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
-          else result ++= basic_string(s.rep)
-        case a: Array =>
-          if (a.is_empty) result ++= "[]"
-          else {
-            result ++= "[\n"
-            a.any.values.foreach { elem =>
-              result ++= inline(elem, indent + 1)
-              result ++= ",\n"
-            }
-            result ++= Symbol.spaces(indent * 2)
-            result += ']'
-          }
-        case table: Table =>
-          if (table.is_empty) result ++= "{}"
-          else {
-            result ++= "{ "
-            Library.separate(None, table.any.values.map(Some(_))).foreach {
-              case None => result ++= ", "
-              case Some((k, v)) =>
-                result ++= key(k)
-                result ++= " = "
-                result ++= inline(v)
+    private def inline(t: T, indent: Int = 0): Str =
+      Library.string_builder() { result =>
+        result ++= Symbol.spaces(indent * 2)
+        (t: @unchecked) match {
+          case s: String =>
+            if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
+            else result ++= basic_string(s.rep)
+          case a: Array =>
+            if (a.is_empty) result ++= "[]"
+            else {
+              result ++= "[\n"
+              a.any.values.foreach { elem =>
+                result ++= inline(elem, indent + 1)
+                result ++= ",\n"
+              }
+              result ++= Symbol.spaces(indent * 2)
+              result += ']'
             }
-            result ++= " }"
-          }
-        case Scalar(s) => result ++= s
-      }
-      result.toString()
-    }
-
-    def apply(toml: Table): Str = {
-      val result = new StringBuilder
-
-      def inline_values(path: List[Key], t: T): Unit =
-        t match {
-          case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) }
-          case _ =>
-            result ++= keys(path.reverse)
-            result ++= " = "
-            result ++= inline(t)
-            result += '\n'
-        }
-
-      def is_inline(elem: T): Bool =
-        elem match {
-          case _: String | _: Integer | _: Float | _: Boolean | _: Offset_Date_Time |
-               _: Local_Date_Time | _: Local_Date | _: Local_Time => true
-          case a: Array => a.any.values.forall(is_inline)
-          case _ => false
-        }
-      def is_table(elem: T): Bool = elem match { case _: Table => true case _ => false }
-
-      def array(path: List[Key], a: Array): Unit =
-        if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table))
-          inline_values(path.take(1), a)
-        else a.table.values.foreach { t =>
-          result ++= "\n[["
-          result ++= keys(path.reverse)
-          result ++= "]]\n"
-          table(path, t, is_table_entry = true)
-        }
-
-      def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = {
-        val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2))
-
-        if (!is_table_entry && path.nonEmpty) {
-          result ++= "\n["
-          result ++= keys(path.reverse)
-          result ++= "]\n"
-        }
-
-        values.foreach { case (k, v) => inline_values(List(k), v) }
-        nodes.foreach {
-          case (k, t: Table) => table(k :: path, t)
-          case (k, arr: Array) => array(k :: path, arr)
-          case _ =>
+          case table: Table =>
+            if (table.is_empty) result ++= "{}"
+            else {
+              result ++= "{ "
+              Library.separate(None, table.any.values.map(Some(_))).foreach {
+                case None => result ++= ", "
+                case Some((k, v)) =>
+                  result ++= key(k)
+                  result ++= " = "
+                  result ++= inline(v)
+              }
+              result ++= " }"
+            }
+          case Scalar(s) => result ++= s
         }
       }
 
-      table(Nil, toml)
-      result.toString
-    }
+    def apply(toml: Table): Str =
+      Library.string_builder() { result =>
+        def inline_values(path: List[Key], t: T): Unit =
+          t match {
+            case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) }
+            case _ =>
+              result ++= keys(path.reverse)
+              result ++= " = "
+              result ++= inline(t)
+              result += '\n'
+          }
+
+        def is_inline(elem: T): Bool =
+          elem match {
+            case _: String | _: Integer | _: Float | _: Boolean | _: Offset_Date_Time |
+                 _: Local_Date_Time | _: Local_Date | _: Local_Time => true
+            case a: Array => a.any.values.forall(is_inline)
+            case _ => false
+          }
+        def is_table(elem: T): Bool = elem match { case _: Table => true case _ => false }
+
+        def array(path: List[Key], a: Array): Unit =
+          if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table))
+            inline_values(path.take(1), a)
+          else a.table.values.foreach { t =>
+            result ++= "\n[["
+            result ++= keys(path.reverse)
+            result ++= "]]\n"
+            table(path, t, is_table_entry = true)
+          }
+
+        def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = {
+          val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2))
+
+          if (!is_table_entry && path.nonEmpty) {
+            result ++= "\n["
+            result ++= keys(path.reverse)
+            result ++= "]\n"
+          }
+
+          values.foreach { case (k, v) => inline_values(List(k), v) }
+          nodes.foreach {
+            case (k, t: Table) => table(k :: path, t)
+            case (k, arr: Array) => array(k :: path, arr)
+            case _ =>
+          }
+        }
+
+        table(Nil, toml)
+      }
   }
 }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/General/utf8.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -20,12 +20,12 @@
   def relevant(s: CharSequence): Boolean = {
     var i = 0
     val n = s.length
-    var utf8 = false
-    while (i < n && !utf8) {
-      if (s.charAt(i) >= 128) { utf8 = true }
+    var found = false
+    while (i < n && !found) {
+      if (s.charAt(i) >= 128) { found = true }
       i += 1
     }
-    utf8
+    found
   }
 
 
@@ -41,8 +41,7 @@
     var rest = 0
     def flush(): Unit = {
       if (code != -1) {
-        if (rest == 0 && Character.isValidCodePoint(code))
-          buf.appendCodePoint(code)
+        if (rest == 0 && Character.isValidCodePoint(code)) buf.appendCodePoint(code)
         else buf.append('\uFFFD')
         code = -1
         rest = 0
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -20,25 +20,24 @@
 
   /* string literals */
 
-  def quote_string(str: String): String = {
-    val result = new StringBuilder(str.length + 10)
-    result += '"'
-    for (s <- Symbol.iterator(str)) {
-      if (s.length == 1) {
-        val c = s(0)
-        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
-          result += '\\'
-          if (c < 10) result += '0'
-          if (c < 100) result += '0'
-          result ++= c.asInstanceOf[Int].toString
+  def quote_string(str: String): String =
+    Library.string_builder(hint = str.length + 10) { result =>
+      result += '"'
+      for (s <- Symbol.iterator(str)) {
+        if (s.length == 1) {
+          val c = s(0)
+          if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
+            result += '\\'
+            if (c < 10) result += '0'
+            if (c < 100) result += '0'
+            result ++= c.asInstanceOf[Int].toString
+          }
+          else result += c
         }
-        else result += c
+        else result ++= s
       }
-      else result ++= s
+      result += '"'
     }
-    result += '"'
-    result.toString
-  }
 }
 
 final class Outer_Syntax private(
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import scala.annotation.tailrec
+
 
 object XML {
   /** XML trees **/
@@ -15,9 +17,14 @@
   type Attribute = Properties.Entry
   type Attributes = Properties.T
 
-  sealed abstract class Tree { override def toString: String = string_of_tree(this) }
+  trait Trav
+  case class End(name: String) extends Trav
+
+  sealed abstract class Tree extends Trav {
+    override def toString: String = string_of_tree(this)
+  }
   type Body = List[Tree]
-  case class Elem(markup: Markup, body: Body) extends Tree {
+  case class Elem(markup: Markup, body: Body) extends Tree with Trav {
     private lazy val hash: Int = (markup, body).hashCode()
     override def hashCode(): Int = hash
 
@@ -29,11 +36,31 @@
 
     def + (att: Attribute): Elem = Elem(markup + att, body)
   }
-  case class Text(content: String) extends Tree {
+  case class Text(content: String) extends Tree with Trav {
     private lazy val hash: Int = content.hashCode()
     override def hashCode(): Int = hash
   }
 
+  trait Traversal {
+    def text(s: String): Unit
+    def elem(markup: Markup, end: Boolean = false): Unit
+    def end_elem(name: String): Unit
+
+    def traverse(trees: List[Tree]): Unit = {
+      @tailrec def trav(list: List[Trav]): Unit =
+        (list : @unchecked) match {
+          case Nil =>
+          case Text(s) :: rest => text(s); trav(rest)
+          case Elem(markup, body) :: rest =>
+            if (markup.is_empty) trav(body ::: rest)
+            else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
+            else { elem(markup); trav(body ::: End(markup.name) :: rest) }
+          case End(name) :: rest => end_elem(name); trav(rest)
+        }
+      trav(trees)
+    }
+  }
+
   def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
   def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
   def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
@@ -95,27 +122,24 @@
 
   /* traverse text */
 
-  def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = {
-    def traverse(x: A, t: Tree): A =
-      t match {
-        case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse)
-        case XML.Elem(_, ts) => ts.foldLeft(x)(traverse)
-        case XML.Text(s) => op(x, s)
+  def traverse_text[A](body: Body, a: A, op: (A, String) => A): A = {
+    @tailrec def trav(x: A, list: List[Tree]): A =
+      list match {
+        case Nil => x
+        case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
+        case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
+        case XML.Text(s) :: rest => trav(op(x, s), rest)
       }
-    body.foldLeft(a)(traverse)
+    trav(a, body)
   }
 
-  def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
-  def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) }
-
-
-  /* text content */
+  def text_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + s.length)
+  def symbol_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + Symbol.length(s))
 
-  def content(body: Body): String = {
-    val text = new StringBuilder(text_length(body))
-    traverse_text(body)(()) { case (_, s) => text.append(s) }
-    text.toString
-  }
+  def content(body: Body): String =
+    Library.string_builder(hint = text_length(body)) { text =>
+      traverse_text(body, (), (_, s) => text.append(s))
+    }
 
   def content(tree: Tree): String = content(List(tree))
 
@@ -125,66 +149,58 @@
 
   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 {
+        str foreach {
+          case '<' => builder ++= "&lt;"
+          case '>' => builder ++= "&gt;"
+          case '&' => builder ++= "&amp;"
+          case '"' if !permissive => builder ++= "&quot;"
+          case '\'' if !permissive => builder ++= "&apos;"
+          case c => 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: List[Tree]): String = { traverse(ts); 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 {
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Fri Jun 28 21:01:57 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,54 @@
 
   /* string representation */
 
-  def traversal(string: String => Unit, body: XML.Body): 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)
-            string(name)
-            for ((a, x) <- atts) { string(Y_string); string(a); string("="); string(x) }
-            string(X_string)
-            ts.foreach(tree)
-            string(XYX_string)
-          }
-        case XML.Text(text) => string(text)
+  trait Output extends XML.Traversal {
+    def byte(b: Byte): Unit
+    def string(s: String): Unit
+
+    // XML.Traversal
+    override def text(s: String): Unit = string(s)
+    override def elem(markup: Markup, end: Boolean = false): Unit = {
+      byte(X_byte)
+      byte(Y_byte)
+      string(markup.name)
+      for ((a, b) <- markup.properties) {
+        byte(Y_byte)
+        string(a)
+        byte('='.toByte)
+        string(b)
       }
-    body.foreach(tree)
+      byte(X_byte)
+      if (end) end_elem(markup.name)
+    }
+    override def end_elem(name: String): Unit = {
+      byte(X_byte)
+      byte(Y_byte)
+      byte(X_byte)
+    }
   }
 
-  def string_of_body(body: XML.Body): String = {
-    val s = new StringBuilder
-    traversal(str => s ++= str, body)
-    s.toString
+  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 ++= recode(s) }
+    def result(ts: List[XML.Tree]): String = { traverse(ts); builder.toString }
+  }
+
+  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 += recode(s) }
   }
 
-  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+  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, recode: String => String = identity): String =
+    string_of_body(List(tree), recode = recode)
+
+  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, recode: String => String = identity): Bytes =
+    bytes_of_body(List(tree), recode = recode)
 
 
   /* parsing */
@@ -67,11 +93,19 @@
     if (name == "") err("unbalanced element")
     else err("unbalanced element " + quote(name))
 
-  private def parse_attrib(source: CharSequence): (String, String) =
-    Properties.Eq.unapply(source.toString) getOrElse err_attribute()
+  def parse_body(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Body = {
+    /* parse + recode */
+
+    def parse_string(s: CharSequence): String = recode(s.toString)
+
+    def parse_attrib(s: CharSequence): (String, String) =
+      Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute()
 
 
-  def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
@@ -100,8 +134,9 @@
       else {
         Library.separated_chunks(is_Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
-            push(name.toString, atts.map(parse_attrib))
-          case txts => for (txt <- txts) add(cache.tree0(XML.Text(cache.string(txt.toString))))
+            push(parse_string(name), atts.map(parse_attrib))
+          case txts =>
+            for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
         }
       }
     }
@@ -111,15 +146,23 @@
     }
   }
 
-  def parse(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
-    parse_body(source, cache = cache) match {
+  def parse(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree =
+    parse_body(source, recode = recode, cache = cache) match {
       case List(result) => result
       case Nil => XML.no_text
       case _ => err("multiple XML trees")
     }
 
-  def parse_elem(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
-    parse_body(source, cache = cache) match {
+  def parse_elem(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree =
+    parse_body(source, recode = recode, cache = cache) match {
       case List(elem: XML.Elem) => elem
       case _ => err("single XML element expected")
     }
@@ -130,13 +173,21 @@
   private def markup_broken(source: CharSequence) =
     XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
-  def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
-    try { parse_body(source, cache = cache) }
+  def parse_body_failsafe(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Body = {
+    try { parse_body(source, recode = recode, cache = cache) }
     catch { case ERROR(_) => List(markup_broken(source)) }
   }
 
-  def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = {
-    try { parse(source, cache = cache) }
+  def parse_failsafe(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree = {
+    try { parse(source, recode = recode, cache = cache) }
     catch { case ERROR(_) => markup_broken(source) }
   }
 }
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/ROOT.ML	Fri Jun 28 21:01:57 2024 +0200
@@ -372,4 +372,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
-
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Jun 28 21:01:57 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, YXML.bytes_of_body(body, recode = Symbol.encode))
   }
 
   sealed case class Aspect(
diff -r 6ed82923d51d -r cba532bf4316 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Pure/library.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -143,10 +143,10 @@
 
   /* strings */
 
-  def make_string(f: StringBuilder => Unit, capacity: Int = 16): String = {
-    val s = new StringBuilder(capacity)
-    f(s)
-    s.toString
+  def string_builder(hint: Int = 0)(body: StringBuilder => Unit): String = {
+    val builder = new StringBuilder(if (hint <= 0) 16 else hint)
+    body(builder)
+    builder.toString
   }
 
   def try_unprefix(prfx: String, s: String): Option[String] =
@@ -194,12 +194,8 @@
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
-    override def toString: String = {
-      val buf = new StringBuilder(length)
-      for (i <- 0 until length)
-        buf.append(charAt(i))
-      buf.toString
-    }
+    override def toString: String =
+      string_builder(hint = length) { buf => for (i <- 0 until length) buf.append(charAt(i)) }
   }
 
   class Line_Termination(text: CharSequence) extends CharSequence {
diff -r 6ed82923d51d -r cba532bf4316 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -251,7 +251,7 @@
 
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
       val lines =
-        XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
+        XML.traverse_text(formatted, if (XML.text_length(formatted) == 0) 0 else 1,
           (n: Int, s: String) => n + Library.count_newlines(s))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
diff -r 6ed82923d51d -r cba532bf4316 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Fri Jun 28 17:13:25 2024 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Fri Jun 28 21:01:57 2024 +0200
@@ -168,14 +168,13 @@
 
     val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym)
 
-    def update_style(text: String): String = {
-      val result = new StringBuilder
-      for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
-        if (Symbol.is_controllable(sym)) result ++= control_decoded
-        result ++= sym
+    def update_style(text: String): String =
+      Library.string_builder() { result =>
+        for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
+          if (Symbol.is_controllable(sym)) result ++= control_decoded
+          result ++= sym
+        }
       }
-      result.toString
-    }
 
     text_area.getSelection.foreach { sel =>
       val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)