aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-08 07:48:57 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-08 07:48:57 -0400
commit815c52605cdba3c95d7e4e6fd3f1eddf0939bc6a (patch)
treeecc04e66934cf2a473b64db35c53847eff7c6f24 /demo
parent87777778aeaee3e1de767499f86bc22789118a69 (diff)
Start 'more' demo with dbgrid
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dbgrid.ur207
-rw-r--r--demo/more/dbgrid.urs93
-rw-r--r--demo/more/dlist.ur88
-rw-r--r--demo/more/dlist.urs13
-rw-r--r--demo/more/grid.ur170
-rw-r--r--demo/more/grid.urp7
-rw-r--r--demo/more/grid.urs35
-rw-r--r--demo/more/grid1.ur52
-rw-r--r--demo/more/grid1.urp6
-rw-r--r--demo/more/grid1.urs1
-rw-r--r--demo/more/prose3
11 files changed, 675 insertions, 0 deletions
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
new file mode 100644
index 00000000..ad7c2789
--- /dev/null
+++ b/demo/more/dbgrid.ur
@@ -0,0 +1,207 @@
+con rawMeta = fn t :: Type =>
+ {New : transaction t,
+ Inj : sql_injectable t}
+
+con colMeta' = fn (row :: {Type}) (t :: Type) =>
+ {Header : string,
+ Project : $row -> transaction t,
+ Update : $row -> t -> transaction ($row),
+ Display : t -> xbody,
+ Edit : t -> xbody,
+ Validate : t -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
+ {Initialize : transaction global_t.1,
+ Handlers : global_t.1 -> colMeta' row global_t.2}
+
+structure Direct = struct
+ con meta = fn global_actual_input :: (Type * Type * Type) =>
+ {Initialize : transaction global_actual_input.1,
+ Handlers : global_actual_input.1
+ -> {Display : global_actual_input.3 -> xbody,
+ Edit : global_actual_input.3 -> xbody,
+ Initialize : global_actual_input.2 -> transaction global_actual_input.3,
+ Parse : global_actual_input.3 -> signal (option global_actual_input.2)}}
+
+ con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+ fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
+ (editableState ts) =
+ {Initialize = m.Initialize,
+ Handlers = fn data => {Header = name,
+ Project = fn r => (m.Handlers data).Initialize r.nm,
+ Update = fn r s =>
+ vo <- current ((m.Handlers data).Parse s);
+ return (case vo of
+ None => r
+ | Some v => r -- nm ++ {nm = v}),
+ Display = (m.Handlers data).Display,
+ Edit = (m.Handlers data).Edit,
+ Validate = fn s => vo <- (m.Handlers data).Parse s; return (Option.isSome vo)}}
+
+ con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3)
+ fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
+ (readOnlyState ts) =
+ {Initialize = m.Initialize,
+ Handlers = fn data => {Header = name,
+ Project = fn r => (m.Handlers data).Initialize r.nm,
+ Update = fn r _ => return r,
+ Display = (m.Handlers data).Display,
+ Edit = (m.Handlers data).Display,
+ Validate = fn _ => return True}}
+
+ con metaBasic = fn actual_input :: (Type * Type) =>
+ {Display : actual_input.2 -> xbody,
+ Edit : source actual_input.2 -> xbody,
+ Initialize : actual_input.1 -> actual_input.2,
+ Parse : actual_input.2 -> option actual_input.1}
+
+ con basicState = source
+ fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) =
+ {Initialize = return (),
+ Handlers = fn () => {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
+ Edit = m.Edit,
+ Initialize = fn v => source (m.Initialize v),
+ Parse = fn s => v <- signal s; return (m.Parse v)}}
+
+ type intGlobal = unit
+ type intInput = basicState string
+ val int : meta (intGlobal, int, intInput) =
+ basic {Display = fn s => <xml>{[s]}</xml>,
+ Edit = fn s => <xml><ctextbox source={s}/></xml>,
+ Initialize = fn n => show n,
+ Parse = fn v => read v}
+
+ type stringGlobal = unit
+ type stringInput = basicState string
+ val string : meta (stringGlobal, string, stringInput) =
+ basic {Display = fn s => <xml>{[s]}</xml>,
+ Edit = fn s => <xml><ctextbox source={s}/></xml>,
+ Initialize = fn s => s,
+ Parse = fn s => Some s}
+
+ type boolGlobal = unit
+ type boolInput = basicState bool
+ val bool : meta (boolGlobal, bool, boolInput) =
+ basic {Display = fn b => <xml>{[b]}</xml>,
+ Edit = fn s => <xml><ccheckbox source={s}/></xml>,
+ Initialize = fn b => b,
+ Parse = fn b => Some b}
+
+ functor Foreign (M : sig
+ con row :: {Type}
+ con t :: Type
+ val show_t : show t
+ val read_t : read t
+ val eq_t : eq t
+ val inj_t : sql_injectable t
+ con nm :: Name
+ constraint [nm] ~ row
+ table tab : ([nm = t] ++ row)
+ val render : $([nm = t] ++ row) -> string
+ end) = struct
+ open M
+
+ con global = list (t * string)
+ con input = source string * t * $row
+
+ val getChoices = List.mapQuery (SELECT * FROM tab AS T)
+ (fn r => (r.T.nm, render r.T))
+
+ fun getChoice k =
+ r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]});
+ return r.T
+
+ val meta =
+ {Initialize = getChoices,
+ Handlers = fn choices =>
+ {Display = fn (_, k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
+ Edit = fn (s, k, _) =>
+ <xml><cselect source={s}>
+ {List.mapX (fn (k', rend) =>
+ <xml><coption value={show k'} selected={k' = k}>{[rend]}</coption>
+ </xml>)
+ choices}
+ </cselect></xml>,
+ Initialize = fn k => s <- source (show k);
+ r <- rpc (getChoice k);
+ return (s, k, r),
+ Parse = fn (s, _, _) => k <- signal s; return (read k)}}
+ end
+end
+
+con computedState = (unit, xbody)
+fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
+ {Initialize = return (),
+ Handlers = fn () => {Header = name,
+ Project = fn r => return <xml>{[f r]}</xml>,
+ Update = fn r _ => return r,
+ Display = fn x => x,
+ Edit = fn _ => <xml>...</xml>,
+ Validate = fn _ => return True}}
+fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
+ {Initialize = return (),
+ Handlers = fn () => {Header = name,
+ Project = fn r => return (f r),
+ Update = fn r _ => return r,
+ Display = fn x => x,
+ Edit = fn _ => <xml>...</xml>,
+ Validate = fn _ => return True}}
+
+functor Make(M : sig
+ con key :: {Type}
+ con row :: {Type}
+ constraint key ~ row
+ table tab : (key ++ row)
+
+ val raw : $(map rawMeta (key ++ row))
+
+ con cols :: {(Type * Type)}
+ val cols : $(map (colMeta (key ++ row)) cols)
+
+ val keyFolder : folder key
+ val rowFolder : folder row
+ val colsFolder : folder cols
+ end) = struct
+ open Grid.Make(struct
+ val list = query (SELECT * FROM {{M.tab}} AS T) (fn r rs => return (r.T :: rs)) []
+
+ val wholeRow = @Folder.concat ! M.keyFolder M.rowFolder
+
+ fun ensql [env] (r : $(M.key ++ M.row)) =
+ map2 [rawMeta] [id] [sql_exp env [] []]
+ (fn [t] meta v => @sql_inject meta.Inj v)
+ [_] wholeRow M.raw r
+
+ val new =
+ row <- Monad.mapR [rawMeta] [id]
+ (fn [nm :: Name] [t :: Type] meta => meta.New)
+ [_] wholeRow M.raw;
+ dml (insert M.tab (ensql row));
+ return row
+
+ fun selector (r : $(M.key ++ M.row)) : sql_exp [T = M.key ++ M.row] [] [] bool =
+ foldR2 [rawMeta] [id]
+ [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool]
+ (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
+ (meta : rawMeta t) (v : t)
+ (exp : rest :: {Type} -> [rest ~ key] => sql_exp [T = key ++ rest] [] [] bool)
+ [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
+ (WHERE T.{nm} = {@sql_inject meta.Inj v} AND {exp [[nm = t] ++ rest] !}))
+ (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
+ [_] M.keyFolder (M.raw --- map rawMeta M.row) (r --- M.row)
+ [_] !
+
+ fun save {Old = row, New = row'} =
+ dml (update [M.key ++ M.row] !
+ (ensql row')
+ M.tab
+ (selector row))
+
+ fun delete row =
+ dml (Basis.delete M.tab (selector row))
+
+ val cols = M.cols
+
+ val folder = M.colsFolder
+ end)
+end
diff --git a/demo/more/dbgrid.urs b/demo/more/dbgrid.urs
new file mode 100644
index 00000000..5f51fcd4
--- /dev/null
+++ b/demo/more/dbgrid.urs
@@ -0,0 +1,93 @@
+con rawMeta = fn t :: Type =>
+ {New : transaction t,
+ Inj : sql_injectable t}
+
+con colMeta' = fn (row :: {Type}) (t :: Type) =>
+ {Header : string,
+ Project : $row -> transaction t,
+ Update : $row -> t -> transaction ($row),
+ Display : t -> xbody,
+ Edit : t -> xbody,
+ Validate : t -> signal bool}
+
+con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
+ {Initialize : transaction global_t.1,
+ Handlers : global_t.1 -> colMeta' row global_t.2}
+
+structure Direct : sig
+ con meta = fn global_actual_input :: (Type * Type * Type) =>
+ {Initialize : transaction global_actual_input.1,
+ Handlers : global_actual_input.1
+ -> {Display : global_actual_input.3 -> xbody,
+ Edit : global_actual_input.3 -> xbody,
+ Initialize : global_actual_input.2 -> transaction global_actual_input.3,
+ Parse : global_actual_input.3 -> signal (option global_actual_input.2)}}
+
+ con editableState :: (Type * Type * Type) -> (Type * Type)
+ val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
+ -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
+ -> colMeta ([nm = ts.2] ++ rest)
+ (editableState ts)
+
+ con readOnlyState :: (Type * Type * Type) -> (Type * Type)
+ val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
+ -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
+ -> colMeta ([nm = ts.2] ++ rest)
+ (readOnlyState ts)
+
+ type intGlobal
+ type intInput
+ val int : meta (intGlobal, int, intInput)
+
+ type stringGlobal
+ type stringInput
+ val string : meta (stringGlobal, string, stringInput)
+
+ type boolGlobal
+ type boolInput
+ val bool : meta (boolGlobal, bool, boolInput)
+
+ functor Foreign (M : sig
+ con row :: {Type}
+ con t :: Type
+ val show_t : show t
+ val read_t : read t
+ val eq_t : eq t
+ val inj_t : sql_injectable t
+ con nm :: Name
+ constraint [nm] ~ row
+ table tab : ([nm = t] ++ row)
+ val render : $([nm = t] ++ row) -> string
+ end) : sig
+ con global :: Type
+ con input :: Type
+ val meta : meta (global, M.t, input)
+ end
+end
+
+con computedState :: (Type * Type)
+val computed : row ::: {Type} -> t ::: Type -> show t
+ -> string -> ($row -> t) -> colMeta row computedState
+val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
+
+functor Make(M : sig
+ con key :: {Type}
+ con row :: {Type}
+ constraint key ~ row
+ table tab : (key ++ row)
+
+ val raw : $(map rawMeta (key ++ row))
+
+ con cols :: {(Type * Type)}
+ val cols : $(map (colMeta (key ++ row)) cols)
+
+ val keyFolder : folder key
+ val rowFolder : folder row
+ val colsFolder : folder cols
+ end) : sig
+ type grid
+
+ val grid : transaction grid
+ val sync : grid -> transaction unit
+ val render : grid -> xbody
+end
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
new file mode 100644
index 00000000..f8aca1e2
--- /dev/null
+++ b/demo/more/dlist.ur
@@ -0,0 +1,88 @@
+datatype dlist'' t =
+ Nil
+ | Cons of t * source (dlist'' t)
+
+datatype dlist' t =
+ Empty
+ | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
+
+con dlist t = source (dlist' t)
+
+type position = transaction unit
+
+fun headPos [t] (dl : dlist t) =
+ dl' <- get dl;
+ case dl' of
+ Nonempty { Head = Cons (_, tl), Tail = tl' } =>
+ cur <- get tl;
+ set dl (case cur of
+ Nil => Empty
+ | _ => Nonempty {Head = cur, Tail = tl'})
+ | _ => return ()
+
+fun tailPos [t] (cur : source (dlist'' t)) new tail =
+ new' <- get new;
+ set cur new';
+
+ case new' of
+ Nil => set tail cur
+ | _ => return ()
+
+val create = fn [t] => source Empty
+
+fun clear [t] (s : dlist t) = set s Empty
+
+fun append [t] dl v =
+ dl' <- get dl;
+ case dl' of
+ Empty =>
+ tl <- source Nil;
+ tl' <- source tl;
+ set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
+ return (headPos dl)
+
+ | Nonempty {Tail = tl, ...} =>
+ cur <- get tl;
+ new <- source Nil;
+ set cur (Cons (v, new));
+ set tl new;
+ return (tailPos cur new tl)
+
+fun render [ctx] [ctx ~ body] [t] f dl = <xml>
+ <dyn signal={dl' <- signal dl;
+ return (case dl' of
+ Empty => <xml/>
+ | Nonempty {Head = hd, Tail = tlTop} =>
+ let
+ fun render' prev dl'' =
+ case dl'' of
+ Nil => <xml/>
+ | Cons (v, tl) =>
+ let
+ val pos = case prev of
+ None => headPos dl
+ | Some prev => tailPos prev tl tlTop
+ in
+ <xml>{f v pos}<dyn signal={tl' <- signal tl;
+ return (render' (Some tl) tl')}/></xml>
+ end
+ in
+ render' None hd
+ end)}/>
+</xml>
+
+fun delete pos = pos
+
+fun elements' [t] (dl'' : dlist'' t) =
+ case dl'' of
+ Nil => return []
+ | Cons (x, dl'') =>
+ dl'' <- signal dl'';
+ tl <- elements' dl'';
+ return (x :: tl)
+
+fun elements [t] (dl : dlist t) =
+ dl' <- signal dl;
+ case dl' of
+ Empty => return []
+ | Nonempty {Head = hd, ...} => elements' hd
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
new file mode 100644
index 00000000..872dabcd
--- /dev/null
+++ b/demo/more/dlist.urs
@@ -0,0 +1,13 @@
+con dlist :: Type -> Type
+type position
+
+val create : t ::: Type -> transaction (dlist t)
+val clear : t ::: Type -> dlist t -> transaction unit
+val append : t ::: Type -> dlist t -> t -> transaction position
+val delete : position -> transaction unit
+val elements : t ::: Type -> dlist t -> signal (list t)
+
+val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
+ -> (t -> position -> xml (ctx ++ body) [] [])
+ -> dlist t
+ -> xml (ctx ++ body) [] []
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
new file mode 100644
index 00000000..e09a1ef0
--- /dev/null
+++ b/demo/more/grid.ur
@@ -0,0 +1,170 @@
+con colMeta' = fn (row :: Type) (t :: Type) =>
+ {Header : string,
+ Project : row -> transaction t,
+ Update : row -> t -> transaction row,
+ Display : t -> xbody,
+ Edit : t -> xbody,
+ Validate : t -> signal bool}
+
+con colMeta = fn (row :: Type) (global_t :: (Type * Type)) =>
+ {Initialize : transaction global_t.1,
+ Handlers : global_t.1 -> colMeta' row global_t.2}
+
+functor Make(M : sig
+ type row
+ val list : transaction (list row)
+ val new : transaction row
+ val save : {Old : row, New : row} -> transaction unit
+ val delete : row -> transaction unit
+
+ con cols :: {(Type * Type)}
+ val cols : $(map (colMeta row) cols)
+
+ val folder : folder cols
+ end) = struct
+ style tabl
+ style tr
+ style th
+ style td
+
+ fun make (row : M.row) [t] (m : colMeta' M.row t) : transaction t = m.Project row
+
+ fun makeAll cols row = @@Monad.exec [transaction] _ [map snd M.cols]
+ (map2 [fst] [colMeta M.row] [fn p :: (Type * Type) => transaction p.2]
+ (fn [p] data meta => make row [_] (meta.Handlers data))
+ [_] M.folder cols M.cols)
+ (@@Folder.mp [_] [_] M.folder)
+
+ fun addRow cols rows row =
+ rowS <- source row;
+ cols <- makeAll cols row;
+ colsS <- source cols;
+ ud <- source False;
+ Monad.ignore (Dlist.append rows {Row = rowS,
+ Cols = colsS,
+ Updating = ud})
+
+ type grid = {Cols : $(map fst M.cols),
+ Rows : Dlist.dlist {Row : source M.row, Cols : source ($(map snd M.cols)), Updating : source bool}}
+
+ val createMetas = Monad.mapR [colMeta M.row] [fst]
+ (fn [nm :: Name] [p :: (Type * Type)] meta => meta.Initialize)
+ [_] M.folder M.cols
+
+ val grid =
+ cols <- createMetas;
+ rows <- Dlist.create;
+ return {Cols = cols, Rows = rows}
+
+ fun sync {Cols = cols, Rows = rows} =
+ Dlist.clear rows;
+ init <- rpc M.list;
+ List.app (addRow cols rows) init
+
+ fun render grid = <xml>
+ <table class={tabl}>
+ <tr class={tr}>
+ <th/> <th/>
+ {foldRX2 [fst] [colMeta M.row] [_]
+ (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}] [[nm] ~ rest]
+ data (meta : colMeta M.row p) =>
+ <xml><th class={th}>{[(meta.Handlers data).Header]}</th></xml>)
+ [_] M.folder grid.Cols M.cols}
+ </tr>
+
+ {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud} pos =>
+ let
+ val delete =
+ Dlist.delete pos;
+ row <- get rowS;
+ rpc (M.delete row)
+
+ val update = set ud True
+
+ val cancel =
+ set ud False;
+ row <- get rowS;
+ cols <- makeAll grid.Cols row;
+ set colsS cols
+
+ val save =
+ cols <- get colsS;
+ errors <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => option string]
+ (fn [nm :: Name] [p :: (Type * Type)] [rest :: {(Type * Type)}]
+ [[nm] ~ rest] data meta v errors =>
+ b <- current ((meta.Handlers data).Validate v);
+ return (if b then
+ errors
+ else
+ case errors of
+ None => Some ((meta.Handlers data).Header)
+ | Some s => Some ((meta.Handlers data).Header
+ ^ ", " ^ s)))
+ None [_] M.folder grid.Cols M.cols cols;
+
+ case errors of
+ Some s => alert ("Can't save because the following columns have invalid values:\n"
+ ^ s)
+ | None =>
+ set ud False;
+ row <- get rowS;
+ row' <- Monad.foldR3 [fst] [colMeta M.row] [snd] [fn _ => M.row]
+ (fn [nm :: Name] [t :: (Type * Type)]
+ [rest :: {(Type * Type)}]
+ [[nm] ~ rest] data meta v row' =>
+ (meta.Handlers data).Update row' v)
+ row [_] M.folder grid.Cols M.cols cols;
+ rpc (M.save {Old = row, New = row'});
+ set rowS row';
+
+ cols <- makeAll grid.Cols row';
+ set colsS cols
+ in
+ <xml><tr class={tr}>
+ <td>
+ <dyn signal={b <- signal ud;
+ return (if b then
+ <xml><button value="Save" onclick={save}/></xml>
+ else
+ <xml><button value="Update" onclick={update}/></xml>)}/>
+ </td>
+ <td><dyn signal={b <- signal ud;
+ return (if b then
+ <xml><button value="Cancel" onclick={cancel}/></xml>
+ else
+ <xml><button value="Delete" onclick={delete}/></xml>)}/>
+ </td>
+
+ <dyn signal={cols <- signal colsS;
+ return (foldRX3 [fst] [colMeta M.row] [snd] [_]
+ (fn [nm :: Name] [t :: (Type * Type)]
+ [rest :: {(Type * Type)}]
+ [[nm] ~ rest] data meta v =>
+ <xml><td class={td}>
+ <dyn signal={b <- signal ud;
+ return (if b then
+ (meta.Handlers data).Edit v
+ else
+ (meta.Handlers data).Display
+ v)}/>
+ <dyn signal={b <- signal ud;
+ if b then
+ valid <-
+ (meta.Handlers data).Validate v;
+ return (if valid then
+ <xml/>
+ else
+ <xml>!</xml>)
+ else
+ return <xml/>}/>
+ </td></xml>)
+ [_] M.folder grid.Cols M.cols cols)}/>
+ </tr></xml>
+ end) grid.Rows}
+ </table>
+
+ <button value="New row" onclick={row <- rpc M.new;
+ addRow grid.Cols grid.Rows row}/>
+ <button value="Refresh" onclick={sync grid}/>
+ </xml>
+end
diff --git a/demo/more/grid.urp b/demo/more/grid.urp
new file mode 100644
index 00000000..0736e4fe
--- /dev/null
+++ b/demo/more/grid.urp
@@ -0,0 +1,7 @@
+
+$/option
+$/monad
+$/list
+dlist
+grid
+dbgrid
diff --git a/demo/more/grid.urs b/demo/more/grid.urs
new file mode 100644
index 00000000..191ec49a
--- /dev/null
+++ b/demo/more/grid.urs
@@ -0,0 +1,35 @@
+con colMeta' = fn (row :: Type) (t :: Type) =>
+ {Header : string,
+ Project : row -> transaction t,
+ Update : row -> t -> transaction row,
+ Display : t -> xbody,
+ Edit : t -> xbody,
+ Validate : t -> signal bool}
+
+con colMeta = fn (row :: Type) (global_t :: (Type * Type)) =>
+ {Initialize : transaction global_t.1,
+ Handlers : global_t.1 -> colMeta' row global_t.2}
+
+functor Make(M : sig
+ type row
+ val list : transaction (list row)
+ val new : transaction row
+ val save : {Old : row, New : row} -> transaction unit
+ val delete : row -> transaction unit
+
+ con cols :: {(Type * Type)}
+ val cols : $(map (colMeta row) cols)
+
+ val folder : folder cols
+ end) : sig
+ type grid
+
+ val grid : transaction grid
+ val sync : grid -> transaction unit
+ val render : grid -> xbody
+
+ style tabl
+ style tr
+ style th
+ style td
+end
diff --git a/demo/more/grid1.ur b/demo/more/grid1.ur
new file mode 100644
index 00000000..43d3aa3d
--- /dev/null
+++ b/demo/more/grid1.ur
@@ -0,0 +1,52 @@
+open Dbgrid
+
+table t1 : {Id : int, A : string}
+ PRIMARY KEY Id
+
+sequence s
+table t : {Id : int, A : int, B : string, C : bool, D : int}
+ PRIMARY KEY Id,
+ CONSTRAINT Foreign FOREIGN KEY (D) REFERENCES t1(Id) ON DELETE CASCADE
+
+fun page (n, s) = return <xml>A = {[n]}, B = {[s]}</xml>
+
+open Make(struct
+ val tab = t
+ con key = [Id = _]
+
+ val raw = {Id = {New = nextval s,
+ Inj = _},
+ A = {New = return 0,
+ Inj = _},
+ B = {New = return "",
+ Inj = _},
+ C = {New = return False,
+ Inj = _},
+ D = {New = return 0,
+ Inj = _}}
+
+ structure F = Direct.Foreign(struct
+ con nm = #Id
+ val tab = t1
+ fun render r = r.A
+ end)
+
+ val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int,
+ A = Direct.editable [#A] ! "A" Direct.int,
+ B = Direct.editable [#B] ! "B" Direct.string,
+ C = Direct.editable [#C] ! "C" Direct.bool,
+ D = Direct.editable [#D] ! "D" F.meta,
+ DA = computed "2A" (fn r => 2 * r.A),
+ Link = computedHtml "Link" (fn r => <xml><a link={page (r.A, r.B)}>Go</a></xml>)}
+ end)
+
+fun main () =
+ grid <- grid;
+ return <xml>
+ <head>
+ <link rel="stylesheet" type="text/css" href="/defun/grid.css"/>
+ </head>
+ <body onload={sync grid}>
+ {render grid}
+ </body>
+ </xml>
diff --git a/demo/more/grid1.urp b/demo/more/grid1.urp
new file mode 100644
index 00000000..8276d4ae
--- /dev/null
+++ b/demo/more/grid1.urp
@@ -0,0 +1,6 @@
+database dbname=test
+library grid
+sql grid.sql
+allow url /defun/grid.css
+
+grid1
diff --git a/demo/more/grid1.urs b/demo/more/grid1.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/more/grid1.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/more/prose b/demo/more/prose
new file mode 100644
index 00000000..37a79724
--- /dev/null
+++ b/demo/more/prose
@@ -0,0 +1,3 @@
+<p>These are some extra demo applications written in <a href="http://www.impredicative.com/ur/">Ur/Web</a>. See <a href="http://www.impredicative.com/ur/demo/">the main demo</a> for a more tutorial-like progression through language and library features.</p>
+
+grid1.urp