tuned signature;

--- a/src/Pure/General/json.scala	Mon Aug 22 15:00:46 2022 +0200
+++ b/src/Pure/General/json.scala	Mon Aug 22 21:25:12 2022 +0200
@@ -253,7 +253,7 @@
 
     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 =
+    def pretty_print(x: T, margin: Int = Pretty.default_margin.toInt): JSON.S =
       Pretty.string_of(List(pretty(x)), margin = margin.toDouble)
   }