diff json.ur @ 18:6cd839818393

Adjust to name change for [Top.id]
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Dec 2011 14:15:02 -0500
parents 8f7396495045
children 8de201d70b91
line wrap: on
line diff
--- a/json.ur	Thu Dec 29 10:10:50 2011 -0500
+++ b/json.ur	Thu Dec 29 14:15:02 2011 -0500
@@ -205,7 +205,7 @@
     end
 
 fun json_record [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json $ts =
-    {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [id] [fn _ => string]
+    {ToJson = fn r => "{" ^ @foldR3 [json] [fn _ => string] [ident] [fn _ => string]
                              (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] (j : json t) name v acc =>
                                  escape name ^ ":" ^ j.ToJson v ^ (case acc of
                                                                        "" => ""
@@ -259,9 +259,9 @@
                                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 =>
-                                                                         case v of
-                                                                             None => error <xml>Missing JSON object field {[name]}</xml>
-                                                                           | Some v => v) fl r names, s')
+                               (@map2 [option] [fn _ => string] [ident] (fn [t] (v : option t) name =>
+                                                                            case v of
+                                                                                None => error <xml>Missing JSON object field {[name]}</xml>
+                                                                              | Some v => v) fl r names, s')
                            end
                    end}