src/Pure/General/latex.scala

       '8' -> "EIGHT",
       '9' -> "NINE")
 
   def output_name(name: String): String =
     if (name.exists(output_name_map.keySet)) {
-      val res = new StringBuilder
-      for (c <- name) {
-        output_name_map.get(c) match {
-          case None => res += c
-          case Some(s) => res ++= s
+      Library.string_builder() { res =>
+        for (c <- name) {
+          output_name_map.get(c) match {
+            case None => res += c
+            case Some(s) => res ++= s
+          }
         }
       }
-      res.toString
     }
     else name
 
 
   /* index entries */
 
   def index_escape(str: String): String = {
     val special1 = "!\"@|"
     val special2 = "\\{}#"
     if (str.exists(c => special1.contains(c) || special2.contains(c))) {
-      val res = new StringBuilder
-      for (c <- str) {
-        if (special1.contains(c)) {
-          res ++= "\\char"
-          res ++= Value.Int(c)
+      Library.string_builder() { res =>
+        for (c <- str) {
+          if (special1.contains(c)) {
+            res ++= "\\char"
+            res ++= Value.Int(c)
+          }
+          else {
+            if (special2.contains(c)) { res += '"'}
+            res += c
+          }
         }
-        else {
-          if (special2.contains(c)) { res += '"'}
-          res += c
-        }
-      }
-      res.toString
+      }
     }
     else str
   }
 
   object Index_Item {