slightly faster XML output: avoid too much regrowing of StringBuilder;

--- 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)

--- 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
   }