src/Pure/General/json.scala

--- a/src/Pure/General/json.scala	Fri Jun 28 11:09:58 2024 +0200
+++ b/src/Pure/General/json.scala	Fri Jun 28 11:37:13 2024 +0200
@@ -196,49 +196,44 @@
         case _ => false
       }
 
-    def apply(json: T): S = {
-      val result = new StringBuilder
-
-      def output(x: T): Unit = {
-        if (!output_atom(x, result)) {
-          x match {
-            case Object(obj) =>
-              result += '{'
-              Library.separate(None, obj.toList.map(Some(_))).foreach({
-                case None => result += ','
-                case Some((x, y)) =>
-                  output_string(x, result)
-                  result += ':'
-                  output(y)
-              })
-              result += '}'
-            case list: List[T] =>
-              result += '['
-              Library.separate(None, list.map(Some(_))).foreach({
-                case None => result += ','
-                case Some(x) => output(x)
-              })
-              result += ']'
-            case _ => error("Bad JSON value: " + x.toString)
+    def apply(json: T): S =
+      Library.string_builder() { result =>
+        def output(x: T): Unit = {
+          if (!output_atom(x, result)) {
+            x match {
+              case Object(obj) =>
+                result += '{'
+                Library.separate(None, obj.toList.map(Some(_))).foreach({
+                  case None => result += ','
+                  case Some((x, y)) =>
+                    output_string(x, result)
+                    result += ':'
+                    output(y)
+                })
+                result += '}'
+              case list: List[T] =>
+                result += '['
+                Library.separate(None, list.map(Some(_))).foreach({
+                  case None => result += ','
+                  case Some(x) => output(x)
+                })
+                result += ']'
+              case _ => error("Bad JSON value: " + x.toString)
+            }
           }
         }
+
+        output(json)
       }
 
-      output(json)
-      result.toString
-    }
-
     private def pretty_atom(x: T): Option[XML.Tree] = {
       val result = new StringBuilder
       val ok = output_atom(x, result)
       if (ok) Some(XML.Text(result.toString)) else None
     }
 
-    private def pretty_string(s: String): XML.Tree = {
-      val result = new StringBuilder
-      output_string(s, result)
-      XML.Text(result.toString)
-    }
+    private def pretty_string(s: String): XML.Tree =
+      XML.Text(Library.string_builder()(output_string(s, _)))
 
     private def pretty_tree(x: T): XML.Tree =
       x match {