aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ur/json.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2018-06-04 11:51:00 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2018-06-04 11:51:00 -0400
commite626ef35ebd7d79a820ead03a8d30d5ee090671c (patch)
tree1f1a2129eff0d6e99f18ec96707720ce30d411ef /lib/ur/json.ur
parentc68da19be2a3fab584973c4a9d0a93035a6d9116 (diff)
parent71dab68defc48d9be9d1e45e63925d0fb01ebb34 (diff)
Merge branch 'master' of ssh://github.com/urweb/urweb
Diffstat (limited to 'lib/ur/json.ur')
-rw-r--r--lib/ur/json.ur4
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/ur/json.ur b/lib/ur/json.ur
index 1e3e3f39..817ec16e 100644
--- a/lib/ur/json.ur
+++ b/lib/ur/json.ur
@@ -52,6 +52,8 @@ fun escape s =
| #"\t" => "\\t"
| #"\"" => "\\\""
| #"\'" => "\\\'"
+ | #"\\" => "\\\\"
+ | #"/" => "\\/"
| x => String.str ch
) ^ esc (String.suffix s 1)
end
@@ -100,6 +102,8 @@ fun unescape s =
| #"t" => "\t"
| #"\"" => "\""
| #"\'" => "\'"
+ | #"\\" => "\\"
+ | #"/" => "/"
| x => error <xml>JSON unescape: Bad escape char: {[x]}</xml>)
^
unesc (i+2)