# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1417740771 18000
# Node ID 4e673b5354346332df2785393528d048e237bde3
# Parent  7530b2b54353ce0871ce08f26a816e1ea7dd5683
Optimizing JSON generation

diff -r 7530b2b54353 -r 4e673b535434 json.ur
--- a/json.ur	Sun Jul 29 12:27:36 2012 -0400
+++ b/json.ur	Thu Dec 04 19:52:51 2014 -0500
@@ -39,22 +39,20 @@
 
 fun escape s =
     let
-        val len = String.length s
-
-        fun esc i =
-            if i >= len then
-                "\""
-            else
+        fun esc s =
+            case s of
+                "" => "\""
+              | _ =>
                 let
-                    val ch = String.sub s i
+                    val ch = String.sub s 0
                 in
                     (if ch = #"\"" || ch = #"\\" then
                          "\\" ^ String.str ch
                      else
-                         String.str ch) ^ esc (i+1)
+                         String.str ch) ^ esc (String.suffix s 1)
                 end
     in
-        "\"" ^ esc 0
+        "\"" ^ esc s
     end
 
 fun unescape s =
@@ -210,7 +208,7 @@
                              (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
                                  escape name ^ ":" ^ j.ToJson v ^ (case acc of
                                                                        "" => ""
-                                                                     | _ => "," ^ acc))
+                                                                     | acc => "," ^ acc))
                              "" fl jss names r ^ "}",
      FromJson = fn s =>
                    let