diff json.ur @ 4:8f7396495045

JSON nulls
author Adam Chlipala <adam@chlipala.net>
date Thu, 02 Dec 2010 12:27:30 -0500
parents 189245a3c075
children 6cd839818393
line wrap: on
line diff
--- a/json.ur	Thu Dec 02 12:17:51 2010 -0500
+++ b/json.ur	Thu Dec 02 12:27:30 2010 -0500
@@ -140,6 +140,19 @@
                                     else
                                         error <xml>JSON: bad boolean string: {[s]}</xml>}
 
+fun json_option [a] (j : json a) : json (option a) =
+    {ToJson = fn v => case v of
+                          None => "null"
+                        | Some v => j.ToJson v,
+     FromJson = fn s => if String.isPrefix {Full = s, Prefix = "null"} then
+                            (None, String.substring s {Start = 4, Len = String.length s - 4})
+                        else
+                            let
+                                val (v, s') = j.FromJson s
+                            in
+                                (Some v, s')
+                            end}
+
 fun json_list [a] (j : json a) : json (list a) =
     let
         fun toJ' (ls : list a) : string =