annotate demo/more/meta.ur @ 1005:c6e948ec79e9
Saving changes to user list
author |
Adam Chlipala <adamc@hcoop.net> |
date |
Tue, 20 Oct 2009 13:08:42 -0400 |
parents |
a87495bcaeec |
children |
d3af9e54c828 |
rev |
line source |
adamc@1004
|
1 con meta = fn (db :: Type, widget :: Type) =>
|
adamc@1004
|
2 {Nam : string,
|
adamc@1004
|
3 Show : db -> xbody,
|
adamc@1004
|
4 Widget : nm :: Name -> xml form [] [nm = widget],
|
adamc@1004
|
5 WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget],
|
adamc@1004
|
6 Parse : widget -> db,
|
adamc@1004
|
7 Inject : sql_injectable db}
|
adamc@1004
|
8
|
adamc@1004
|
9 fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) name : meta (t, string) =
|
adamc@1004
|
10 {Nam = name,
|
adamc@1004
|
11 Show = txt,
|
adamc@1004
|
12 Widget = fn [nm :: Name] => <xml><textbox{nm}/></xml>,
|
adamc@1004
|
13 WidgetPopulated = fn [nm :: Name] n =>
|
adamc@1004
|
14 <xml><textbox{nm} value={show n}/></xml>,
|
adamc@1004
|
15 Parse = readError,
|
adamc@1004
|
16 Inject = _}
|
adamc@1004
|
17
|
adamc@1004
|
18 val int = default
|
adamc@1004
|
19 val float = default
|
adamc@1004
|
20 val string = default
|
adamc@1004
|
21 fun bool name = {Nam = name,
|
adamc@1004
|
22 Show = txt,
|
adamc@1004
|
23 Widget = fn [nm :: Name] => <xml><checkbox{nm}/></xml>,
|
adamc@1004
|
24 WidgetPopulated = fn [nm :: Name] b =>
|
adamc@1004
|
25 <xml><checkbox{nm} checked={b}/></xml>,
|
adamc@1004
|
26 Parse = fn x => x,
|
adamc@1004
|
27 Inject = _}
|