# HG changeset patch
# User wenzelm
# Date 1637077189 -3600
# Node ID c606fddc5b05490f80a994efa6ea24b287852bb0
# Parent  b6f6e3ca2bdc495e5b87c87b2c64271d5222fb32
slightly faster XML output: avoid too much regrowing of StringBuilder;

diff -r b6f6e3ca2bdc -r c606fddc5b05 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Nov 15 23:52:08 2021 +0100
+++ b/src/Pure/Thy/html.scala	Tue Nov 16 16:39:49 2021 +0100
@@ -233,7 +233,7 @@
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
-    Library.make_string(output(_, body, hidden, structural))
+    Library.make_string(output(_, body, hidden, structural), capacity = XML.text_length(body) * 2)
 
   def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
     output(List(tree), hidden, structural)
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
   }