# HG changeset patch
# User wenzelm
# Date 1719565798 -7200
# Node ID dfadcfdf8dadbde802d99485c353757ce23d0f6f
# Parent  2990f341e0c6cc5ac75972fc3ae5bd71801641fe
tuned signature, following Bytes.Builder.use;

diff -r 2990f341e0c6 -r dfadcfdf8dad src/Pure/General/html.scala
--- a/src/Pure/General/html.scala	Fri Jun 28 00:30:49 2024 +0200
+++ b/src/Pure/General/html.scala	Fri Jun 28 11:09:58 2024 +0200
@@ -224,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)
+    }
   }
 
 
@@ -259,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 2990f341e0c6 -r dfadcfdf8dad src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Jun 28 00:30:49 2024 +0200
+++ b/src/Pure/library.scala	Fri Jun 28 11:09:58 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] =