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] =