Mercurial > urweb
diff lib/ur/top.ur @ 1360:02fc16faecf3
[De]serialization of times in JavaScript; proper integer division in JavaScript; Basis.crypt; Top.mkRead'; more aggressive Mono-level inlining, for values of function-y types
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 23 Dec 2010 17:46:40 -0500 |
| parents | 4172863d049d |
| children | 7dd8a6704265 |
line wrap: on
line diff
--- a/lib/ur/top.ur Thu Dec 23 11:23:31 2010 -0500 +++ b/lib/ur/top.ur Thu Dec 23 17:46:40 2010 -0500 @@ -89,7 +89,7 @@ None => None | v => Some v) -fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) = +fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) : xml ctx use [] = cdata (show v) fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) = @@ -343,3 +343,8 @@ case e2 of None => (SQL {e1} IS NULL) | Some _ => sql_binary sql_eq e1 (sql_inject e2) + +fun mkRead' [t ::: Type] (f : string -> option t) (name : string) : read t = + mkRead (fn s => case f s of + None => error <xml>Invalid {txt name}: {txt s}</xml> + | Some v => v) f