diff -r b6f6e3ca2bdc -r c606fddc5b05 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Nov 15 23:52:08 2021 +0100
+++ b/src/Pure/library.scala	Tue Nov 16 16:39:49 2021 +0100
@@ -129,9 +129,9 @@
 
   /* strings */
 
-  def make_string(f: StringBuilder => Unit): String =
+  def make_string(f: StringBuilder => Unit, capacity: Int = 16): String =
   {
-    val s = new StringBuilder
+    val s = new StringBuilder(capacity)
     f(s)
     s.toString
   }