diff json.ur @ 3:189245a3c075

Wikipedia JSON example working
author Adam Chlipala <adam@chlipala.net>
date Thu, 02 Dec 2010 12:17:51 -0500
parents 478524b9d23a
children 8f7396495045
line wrap: on
line diff
--- a/json.ur	Thu Dec 02 11:59:55 2010 -0500
+++ b/json.ur	Thu Dec 02 12:17:51 2010 -0500
@@ -243,7 +243,7 @@
                            error <xml>JSON record doesn't begin with brace</xml>
                        else
                            let
-                               val (r, s') = fromJ (String.substring s {Start = 1, Len = String.length s - 1})
+                               val (r, s') = fromJ (skipSpaces (String.substring s {Start = 1, Len = String.length s - 1}))
                                                    (@map0 [option] (fn [t ::_] => None) fl)
                            in
                                (@map2 [option] [fn _ => string] [id] (fn [t] (v : option t) name =>