# HG changeset patch
# User wenzelm
# Date 1661196312 -7200
# Node ID 881871e0fa9ec062a71c4dc0c155cd3a9d7a4a35
# Parent  4fe213c214f9c941a7fba30023bde6a20eeee943
tuned signature;

diff -r 4fe213c214f9 -r 881871e0fa9e src/Pure/General/json.scala
--- 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)
   }