summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@csail.mit.edu>2018-06-04 10:21:08 -0400
committerGravatar GitHub <noreply@github.com>2018-06-04 10:21:08 -0400
commit71dab68defc48d9be9d1e45e63925d0fb01ebb34 (patch)
treea6c96c59fb7ca903c9a96ee516a4f1c5534b0a4c
parentea85b40d3a89447dcc65696cb1bb65bcf8806869 (diff)
parent87c86c5d2066a8805c7e72e3279ae8d5822f0c90 (diff)
Merge pull request #126 from majorseitan/master
Improved support for JSON escape characters
-rw-r--r--lib/ur/json.ur4
-rw-r--r--tests/jsonTest.ur2
2 files changed, 5 insertions, 1 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)
diff --git a/tests/jsonTest.ur b/tests/jsonTest.ur
index 38d0d201..bce269bd 100644
--- a/tests/jsonTest.ur
+++ b/tests/jsonTest.ur
@@ -1,7 +1,7 @@
open Json
fun main () : transaction page = return <xml><body>
- <pre>{[ fromJson "\"line 1\\nline 2\"" : string ]}</pre><br/>
+ <pre>{[ fromJson "\"\\\\line \/ 1\\nline 2\"" : string ]}</pre><br/>
<pre>{[fromJson "[1, 2, 3]" : list int]}</pre><br/>
<pre>{[toJson ("hi" :: "bye\"" :: "hehe" :: [])]}</pre>
</body></xml>