# HG changeset patch
# User wenzelm
# Date 1661173246 -7200
# Node ID 4fe213c214f9c941a7fba30023bde6a20eeee943
# Parent  97445e2084194fc2d53477d14c5012094ff5b67b
support for pretty-printing of JSON trees;

diff -r 97445e208419 -r 4fe213c214f9 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Mon Aug 22 14:48:14 2022 +0200
+++ b/src/Pure/General/json.scala	Mon Aug 22 15:00:46 2022 +0200
@@ -165,8 +165,6 @@
       try { Some(parse(s, strict = false)) }
       catch { case ERROR(_) => None }
 
-    def apply_lines(json: List[T]): S = json.map(apply).mkString("[", ",\n", "]")
-
     private def output_string(s: String, result: StringBuilder): Unit = {
       result += '"'
       result ++=
@@ -228,6 +226,35 @@
       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_tree(x: T): XML.Tree =
+      x match {
+        case Object(obj) =>
+          Pretty.`enum`(
+            for ((x, y) <- obj.toList)
+              yield Pretty.block(List(pretty_string(x), XML.Text(":"), Pretty.brk(1), pretty(y))),
+            bg = "{", en = "}", indent = 1)
+        case list: List[T] =>
+          Pretty.`enum`(list.map(pretty), bg = "[", en = "]", indent = 1)
+        case _ => error("Bad JSON value: " + x.toString)
+      }
+
+    def pretty(x: T): XML.Tree = pretty_atom(x) getOrElse pretty_tree(x)
+
+    def pretty_print(x: T, margin: Int = Pretty.default_margin.toInt): String =
+      Pretty.string_of(List(pretty(x)), margin = margin.toDouble)
   }
 
 
diff -r 97445e208419 -r 4fe213c214f9 src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Mon Aug 22 14:48:14 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Mon Aug 22 15:00:46 2022 +0200
@@ -29,7 +29,7 @@
   def make_symbols(): File.Content = {
     val symbols = Symbol.Symbols.load(static = true)
     val symbols_js =
-      JSON.Format.apply_lines(
+      JSON.Format.pretty_print(
         for (entry <- symbols.entries) yield
           JSON.Object(
             "symbol" -> entry.symbol,
@@ -43,7 +43,7 @@
   def make_isabelle_encoding(header: String): File.Content = {
     val symbols = Symbol.Symbols.load(static = true)
     val symbols_js =
-      JSON.Format.apply_lines(
+      JSON.Format.pretty_print(
         for (entry <- symbols.entries; code <- entry.code)
           yield JSON.Object("symbol" -> entry.symbol, "code" -> code))