# HG changeset patch # User Adam Chlipala # Date 1256057333 14400 # Node ID a87495bcaeec2f935967834c26c9c97679663a21 # Parent 61c30f0742d735da33d151455c9e402ed32646b9 Start of user management diff -r 61c30f0742d7 -r a87495bcaeec demo/more/bulkEdit.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/bulkEdit.ur Tue Oct 20 12:48:53 2009 -0400 @@ -0,0 +1,51 @@ +open Meta + +functor Make(M : sig + con keyName :: Name + con keyType :: Type + val showKey : show keyType + + con visible :: {(Type * Type)} + constraint [keyName] ~ visible + val folder : folder visible + val visible : $(map Meta.meta visible) + + con invisible :: {Type} + constraint [keyName] ~ invisible + constraint visible ~ invisible + + val title : string + val isAllowed : transaction bool + table t : ([keyName = keyType] ++ map fst visible ++ invisible) + end) = struct + + open M + + fun main () = + items <- queryX (SELECT t.{keyName}, t.{{map fst visible}} FROM t) + (fn r => + + {useMore (foldR2 [meta] [fst] [fn cols :: {(Type * Type)} => + xml [Body, Form, Tr] [] (map snd cols)] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] + (m : meta p) v (acc : xml [Body, Form, Tr] [] (map snd rest)) => + + {m.WidgetPopulated [nm] v} + {useMore acc} + ) + + [_] folder visible (r.T -- keyName))} + ); + + return +

{[title]}

+ +
+ {foldRX [meta] [_] + (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest] m => + ) [_] folder visible} + {items} +
{[m.Nam]}
+ + +end diff -r 61c30f0742d7 -r a87495bcaeec demo/more/bulkEdit.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/bulkEdit.urs Tue Oct 20 12:48:53 2009 -0400 @@ -0,0 +1,22 @@ +functor Make(M : sig + con keyName :: Name + con keyType :: Type + val showKey : show keyType + + con visible :: {(Type * Type)} + constraint [keyName] ~ visible + val folder : folder visible + val visible : $(map Meta.meta visible) + + con invisible :: {Type} + constraint [keyName] ~ invisible + constraint visible ~ invisible + + val title : string + val isAllowed : transaction bool + table t : ([keyName = keyType] ++ map fst visible ++ invisible) + end) : sig + + val main : unit -> transaction page + +end diff -r 61c30f0742d7 -r a87495bcaeec demo/more/conference.ur --- a/demo/more/conference.ur Tue Oct 20 11:05:58 2009 -0400 +++ b/demo/more/conference.ur Tue Oct 20 12:48:53 2009 -0400 @@ -1,27 +1,4 @@ -con meta = fn (db :: Type, widget :: Type) => - {Show : db -> xbody, - Widget : nm :: Name -> xml form [] [nm = widget], - WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], - Parse : widget -> db, - Inject : sql_injectable db} - -fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) : meta (t, string) = - {Show = txt, - Widget = fn [nm :: Name] => , - WidgetPopulated = fn [nm :: Name] n => - , - Parse = readError, - Inject = _} - -val int = default -val float = default -val string = default -val bool = {Show = txt, - Widget = fn [nm :: Name] => , - WidgetPopulated = fn [nm :: Name] b => - , - Parse = fn x => x, - Inject = _} +open Meta functor Make(M : sig con paper :: {(Type * Type)} @@ -52,7 +29,7 @@ cookie login : {Id : int, Password : string} - fun checkLogin () = + val checkLogin = r <- getCookie login; case r of None => return None @@ -62,6 +39,21 @@ WHERE user.Id = {[r.Id]} AND user.Password = {[r.Password]}) + structure Users = BulkEdit.Make(struct + con keyName = #Id + val visible = {Nam = string "Name", + Chair = bool "Chair?", + OnPc = bool "On PC?"} + + val title = "Users" + val isAllowed = + me <- checkLogin; + return (Option.isSome me) + + val t = user + end) + + fun doRegister r = n <- oneRowE1 (SELECT COUNT( * ) AS N FROM user @@ -90,11 +82,18 @@ and main () = - me <- checkLogin (); + me <- checkLogin; return {case me of None =>
  • Register for access
    •  - | Some {Nam = name, ...} => Welcome, {[name]}!} + | Some me => +
    Welcome, {[me.Nam]}!
    + + {if me.Chair then +
  • Manage users
    •  + else + } + }     end diff -r 61c30f0742d7 -r a87495bcaeec demo/more/conference.urp --- a/demo/more/conference.urp Tue Oct 20 11:05:58 2009 -0400 +++ b/demo/more/conference.urp Tue Oct 20 12:48:53 2009 -0400 @@ -1,3 +1,5 @@ $/option +meta +bulkEdit conference diff -r 61c30f0742d7 -r a87495bcaeec demo/more/conference.urs --- a/demo/more/conference.urs Tue Oct 20 11:05:58 2009 -0400 +++ b/demo/more/conference.urs Tue Oct 20 12:48:53 2009 -0400 @@ -1,23 +1,11 @@ -con meta = fn (db :: Type, widget :: Type) => - {Show : db -> xbody, - Widget : nm :: Name -> xml form [] [nm = widget], - WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], - Parse : widget -> db, - Inject : sql_injectable db} - -val int : meta (int, string) -val float : meta (float, string) -val string : meta (string, string) -val bool : meta (bool, bool) - functor Make(M : sig con paper :: {(Type * Type)} constraint [Id, Title] ~ paper - val paper : $(map meta paper) + val paper : $(map Meta.meta paper) con review :: {(Type * Type)} constraint [Paper, User] ~ review - val review : $(map meta review) + val review : $(map Meta.meta review) end) : sig val main : unit -> transaction page diff -r 61c30f0742d7 -r a87495bcaeec demo/more/meta.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/meta.ur Tue Oct 20 12:48:53 2009 -0400 @@ -0,0 +1,27 @@ +con meta = fn (db :: Type, widget :: Type) => + {Nam : string, + Show : db -> xbody, + Widget : nm :: Name -> xml form [] [nm = widget], + WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], + Parse : widget -> db, + Inject : sql_injectable db} + +fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : meta (t, string) = + {Nam = name, + Show = txt, + Widget = fn [nm :: Name] => , + WidgetPopulated = fn [nm :: Name] n => + , + Parse = readError, + Inject = _} + +val int = default +val float = default +val string = default +fun bool name = {Nam = name, + Show = txt, + Widget = fn [nm :: Name] => , + WidgetPopulated = fn [nm :: Name] b => + , + Parse = fn x => x, + Inject = _} diff -r 61c30f0742d7 -r a87495bcaeec demo/more/meta.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/more/meta.urs Tue Oct 20 12:48:53 2009 -0400 @@ -0,0 +1,12 @@ +con meta = fn (db :: Type, widget :: Type) => + {Nam : string, + Show : db -> xbody, + Widget : nm :: Name -> xml form [] [nm = widget], + WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], + Parse : widget -> db, + Inject : sql_injectable db} + +val int : string -> meta (int, string) +val float : string -> meta (float, string) +val string : string -> meta (string, string) +val bool : string -> meta (bool, bool) diff -r 61c30f0742d7 -r a87495bcaeec lib/ur/basis.urs --- a/lib/ur/basis.urs Tue Oct 20 11:05:58 2009 -0400 +++ b/lib/ur/basis.urs Tue Oct 20 12:48:53 2009 -0400 @@ -594,25 +594,25 @@ Onload = transaction unit] ++ boxEvents) val form : ctx ::: {Unit} -> bind ::: {Type} - -> [[Body] ~ ctx] => - xml form [] bind + -> [[Body, Form] ~ ctx] => + xml ([Body, Form] ++ ctx) [] bind -> xml ([Body] ++ ctx) [] [] val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> [[Form] ~ ctx] => nm :: Name -> [[nm] ~ use] => - xml form [] bind + xml ([Form] ++ ctx) [] bind -> xml ([Form] ++ ctx) use [nm = $bind] val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} - -> [[Form] ~ ctx] => + -> [[Form, Subform] ~ ctx] => nm :: Name -> [[nm] ~ use] => - xml subform [Entry = $bind] [] + xml ([Subform] ++ ctx) [Entry = $bind] [] -> xml ([Form] ++ ctx) use [nm = list ($bind)] val entry : ctx ::: {Unit} -> bind ::: {Type} - -> [[Subform] ~ ctx] => - xml form [] bind + -> [[Subform, Form] ~ ctx] => + xml ([Form] ++ ctx) [] bind -> xml ([Subform] ++ ctx) [Entry = $bind] [] con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => diff -r 61c30f0742d7 -r a87495bcaeec lib/ur/top.ur --- a/lib/ur/top.ur Tue Oct 20 11:05:58 2009 -0400 +++ b/lib/ur/top.ur Tue Oct 20 12:48:53 2009 -0400 @@ -216,10 +216,10 @@ (fn fs _ => f fs) () -fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] +fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] [tables ~ exps] (q : sql_query tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) - -> xml ctx [] []) = + -> xml ctx inp []) = query q (fn fs acc => return {acc}{f fs}) diff -r 61c30f0742d7 -r a87495bcaeec lib/ur/top.urs --- a/lib/ur/top.urs Tue Oct 20 11:05:58 2009 -0400 +++ b/lib/ur/top.urs Tue Oct 20 12:48:53 2009 -0400 @@ -125,12 +125,12 @@ -> transaction unit) -> transaction unit -val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} +val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} -> [tables ~ exps] => sql_query tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) - -> xml ctx [] []) - -> transaction (xml ctx [] []) + -> xml ctx inp []) + -> transaction (xml ctx inp []) val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> [tables ~ exps] =>