# HG changeset patch
# User wenzelm
# Date 1483452470 -3600
# Node ID ae97a5afffcc055fa2bac17762ee96edb1e6bad2
# Parent  8c1557308eb5999e731b876ff352132eb45eff8f
avoid escape of '/' in JSONFormat.quoteString;

diff -r 8c1557308eb5 -r ae97a5afffcc src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Jan 03 14:45:50 2017 +0100
+++ b/src/Pure/General/json.scala	Tue Jan 03 15:07:50 2017 +0100
@@ -32,7 +32,19 @@
       def string(s: String)
       {
         result += '"'
-        result ++= scala.util.parsing.json.JSONFormat.quoteString(s)
+        result ++=
+          s.iterator.map {
+            case '"'  => "\\\""
+            case '\\' => "\\\\"
+            case '\b' => "\\b"
+            case '\f' => "\\f"
+            case '\n' => "\\n"
+            case '\r' => "\\r"
+            case '\t' => "\\t"
+            case c =>
+              if (c <= '\u001f' || c >= '\u007f' && c <= '\u009f') "\\u%04x".format(c.toInt)
+              else c
+          }.mkString
         result += '"'
       }