src/Pure/library.scala

--- a/src/Pure/library.scala	Sun Oct 23 12:27:11 2016 +0200
+++ b/src/Pure/library.scala	Sun Oct 23 12:30:57 2016 +0200
@@ -119,6 +119,13 @@
 
   /* strings */
 
+  def make_string(f: StringBuilder => Unit): String =
+  {
+    val s = new StringBuilder
+    f(s)
+    s.toString
+  }
+
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None