Mercurial > urweb

comparison demo/more/dbgrid.ur @ 961:8c37699de273

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Grid sorting working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 19 Sep 2009 13:32:33 -0400
parents 2412cb10c97c
children fbc3a0eef45a
comparison
equal deleted inserted replaced
960:6f34950825b6 961:8c37699de273
9 Display : input -> xbody, 9 Display : input -> xbody,
10 Edit : input -> xbody, 10 Edit : input -> xbody,
11 Validate : input -> signal bool, 11 Validate : input -> signal bool,
12 CreateFilter : transaction filter, 12 CreateFilter : transaction filter,
13 DisplayFilter : filter -> xbody, 13 DisplayFilter : filter -> xbody,
14 Filter : filter -> $row -> signal bool} 14 Filter : filter -> $row -> signal bool,
15 Sort : option ($row -> $row -> bool)}
15 16
16 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) => 17 con colMeta = fn (row :: {Type}) (global_input_filter :: (Type * Type * Type)) =>
17 {Initialize : transaction global_input_filter.1, 18 {Initialize : transaction global_input_filter.1,
18 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} 19 Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3}
19 20
28 Edit : actual_input_filter.2 -> xbody, 29 Edit : actual_input_filter.2 -> xbody,
29 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2, 30 Initialize : actual_input_filter.1 -> transaction actual_input_filter.2,
30 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1), 31 Parse : actual_input_filter.2 -> signal (option actual_input_filter.1),
31 CreateFilter : transaction actual_input_filter.3, 32 CreateFilter : transaction actual_input_filter.3,
32 DisplayFilter : actual_input_filter.3 -> xbody, 33 DisplayFilter : actual_input_filter.3 -> xbody,
33 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool} 34 Filter : actual_input_filter.3 -> actual_input_filter.1 -> signal bool,
35 Sort : actual_input_filter.1 -> actual_input_filter.1 -> bool}
34 36
35 datatype metaBoth actual input filter = 37 datatype metaBoth actual input filter =
36 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter) 38 NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
37 | Nullable of metaBase (actual, input, filter) 39 | Nullable of metaBase (actual, input, filter)
38 40
56 Display = mr.Display, 58 Display = mr.Display,
57 Edit = mr.Edit, 59 Edit = mr.Edit,
58 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo), 60 Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo),
59 CreateFilter = mr.CreateFilter, 61 CreateFilter = mr.CreateFilter,
60 DisplayFilter = mr.DisplayFilter, 62 DisplayFilter = mr.DisplayFilter,
61 Filter = fn i r => mr.Filter i r.nm} 63 Filter = fn i r => mr.Filter i r.nm,
64 Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
62 in 65 in
63 {Initialize = m.Initialize, 66 {Initialize = m.Initialize,
64 Handlers = fn data => case m.Handlers data of 67 Handlers = fn data => case m.Handlers data of
65 NonNull (mr, _) => doMr mr 68 NonNull (mr, _) => doMr mr
66 | Nullable mr => doMr mr} 69 | Nullable mr => doMr mr}
76 Display = mr.Display, 79 Display = mr.Display,
77 Edit = mr.Display, 80 Edit = mr.Display,
78 Validate = fn _ => return True, 81 Validate = fn _ => return True,
79 CreateFilter = mr.CreateFilter, 82 CreateFilter = mr.CreateFilter,
80 DisplayFilter = mr.DisplayFilter, 83 DisplayFilter = mr.DisplayFilter,
81 Filter = fn i r => mr.Filter i r.nm} 84 Filter = fn i r => mr.Filter i r.nm,
85 Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
82 in 86 in
83 {Initialize = m.Initialize, 87 {Initialize = m.Initialize,
84 Handlers = fn data => case m.Handlers data of 88 Handlers = fn data => case m.Handlers data of
85 NonNull (mr, _) => doMr mr 89 NonNull (mr, _) => doMr mr
86 | Nullable mr => doMr mr} 90 | Nullable mr => doMr mr}
94 IsNull : actual_input_filter.2 -> bool, 98 IsNull : actual_input_filter.2 -> bool,
95 Parse : actual_input_filter.2 -> option actual_input_filter.1, 99 Parse : actual_input_filter.2 -> option actual_input_filter.1,
96 CreateFilter : actual_input_filter.3, 100 CreateFilter : actual_input_filter.3,
97 DisplayFilter : source actual_input_filter.3 -> xbody, 101 DisplayFilter : source actual_input_filter.3 -> xbody,
98 Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool, 102 Filter : actual_input_filter.3 -> actual_input_filter.1 -> bool,
99 FilterIsNull : actual_input_filter.3 -> bool} 103 FilterIsNull : actual_input_filter.3 -> bool,
104 Sort : actual_input_filter.1 -> actual_input_filter.1 -> bool}
100 105
101 con basicState = source 106 con basicState = source
102 con basicFilter = source 107 con basicFilter = source
103 fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) = 108 fun basic [ts ::: (Type * Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2, basicFilter ts.3) =
104 {Initialize = return (), 109 {Initialize = return (),
111 DisplayFilter = m.DisplayFilter, 116 DisplayFilter = m.DisplayFilter,
112 Filter = fn f v => f <- signal f; 117 Filter = fn f v => f <- signal f;
113 return (if m.FilterIsNull f then 118 return (if m.FilterIsNull f then
114 True 119 True
115 else 120 else
116 m.Filter f v)}, 121 m.Filter f v),
122 Sort = m.Sort},
117 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>, 123 {Display = fn s => <xml><dyn signal={v <- signal s; return (m.Display v)}/></xml>,
118 Edit = m.Edit, 124 Edit = m.Edit,
119 Initialize = fn v => source (case v of 125 Initialize = fn v => source (case v of
120 None => m.InitializeNull 126 None => m.InitializeNull
121 | Some v => m.Initialize v), 127 | Some v => m.Initialize v),
132 return (if m.FilterIsNull f then 138 return (if m.FilterIsNull f then
133 True 139 True
134 else 140 else
135 case v of 141 case v of
136 None => False 142 None => False
137 | Some v => m.Filter f v) : signal bool})} 143 | Some v => m.Filter f v),
144 Sort = fn x y =>
145 case (x, y) of
146 (None, _) => True
147 | (Some x', Some y') => m.Sort x' y'
148 | _ => False})}
138 149
139 fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) = 150 fun nullable [global] [actual] [input] [filter] (m : meta (global, actual, input, filter)) =
140 {Initialize = m.Initialize, 151 {Initialize = m.Initialize,
141 Handlers = fn d => case m.Handlers d of 152 Handlers = fn d => case m.Handlers d of
142 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml> 153 Nullable _ => error <xml>Don't stack calls to Direct.nullable!</xml>
156 DisplayFilter = fn s => <xml><ctextbox size={5} source={s}/></xml> : xbody, 167 DisplayFilter = fn s => <xml><ctextbox size={5} source={s}/></xml> : xbody,
157 Filter = fn s n => 168 Filter = fn s n =>
158 case read s of 169 case read s of
159 None => True 170 None => True
160 | Some n' => n' = n, 171 | Some n' => n' = n,
161 FilterIsNull = eq ""} 172 FilterIsNull = eq "",
173 Sort = le}
162 174
163 type stringGlobal = unit 175 type stringGlobal = unit
164 type stringInput = basicState string 176 type stringInput = basicState string
165 type stringFilter = basicFilter string 177 type stringFilter = basicFilter string
166 val string : meta (stringGlobal, string, stringInput, stringFilter) = 178 val string : meta (stringGlobal, string, stringInput, stringFilter) =
174 DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody, 186 DisplayFilter = fn s => <xml><ctextbox source={s}/></xml> : xbody,
175 Filter = fn s n => 187 Filter = fn s n =>
176 case read s of 188 case read s of
177 None => True 189 None => True
178 | Some n' => n' = n, 190 | Some n' => n' = n,
179 FilterIsNull = eq ""} 191 FilterIsNull = eq "",
192 Sort = le}
180 193
181 type boolGlobal = unit 194 type boolGlobal = unit
182 type boolInput = basicState bool 195 type boolInput = basicState bool
183 type boolFilter = basicFilter string 196 type boolFilter = basicFilter string
184 val bool : meta (boolGlobal, bool, boolInput, boolFilter) = 197 val bool : meta (boolGlobal, bool, boolInput, boolFilter) =
197 Filter = fn s b => 210 Filter = fn s b =>
198 case s of 211 case s of
199 "0" => b = False 212 "0" => b = False
200 | "1" => b = True 213 | "1" => b = True
201 | _ => True, 214 | _ => True,
202 FilterIsNull = eq ""} 215 FilterIsNull = eq "",
216 Sort = le}
203 217
204 functor Foreign (M : sig 218 functor Foreign (M : sig
205 con row :: {Type} 219 con row :: {Type}
206 con t :: Type 220 con t :: Type
207 val show_t : show t 221 val show_t : show t
208 val read_t : read t 222 val read_t : read t
209 val eq_t : eq t 223 val eq_t : eq t
224 val ord_t : ord t
210 val inj_t : sql_injectable t 225 val inj_t : sql_injectable t
211 con nm :: Name 226 con nm :: Name
212 constraint [nm] ~ row 227 constraint [nm] ~ row
213 table tab : ([nm = t] ++ row) 228 table tab : ([nm = t] ++ row)
214 val render : $([nm = t] ++ row) -> string 229 val render : $([nm = t] ++ row) -> string
256 choices} 271 choices}
257 </cselect></xml> : xbody, 272 </cselect></xml> : xbody,
258 Filter = fn s k => s <- signal s; 273 Filter = fn s k => s <- signal s;
259 return (case read s : option t of 274 return (case read s : option t of
260 None => True 275 None => True
261 | Some k' => k' = k)}, 276 | Some k' => k' = k),
277 Sort = le},
262 {Display = fn (_, kr) => case kr of 278 {Display = fn (_, kr) => case kr of
263 None => <xml>NULL</xml> 279 None => <xml>NULL</xml>
264 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>, 280 | Some (k, r) => <xml>{[render ({nm = k} ++ r)]}</xml>,
265 Edit = fn (s, kr) => 281 Edit = fn (s, kr) =>
266 <xml><cselect source={s}> 282 <xml><cselect source={s}>
306 | _ => 322 | _ =>
307 case read (String.substring s {Start = 1, 323 case read (String.substring s {Start = 1,
308 Len = String.length s - 1}) 324 Len = String.length s - 1})
309 : option t of 325 : option t of
310 None => True 326 None => True
311 | Some k => ko = Some k)})} 327 | Some k => ko = Some k),
328 Sort = le})}
312 end 329 end
313 end 330 end
314 331
315 con computedState = (unit, xbody, unit) 332 con computedState = (unit, xbody, unit)
316 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState = 333 fun computed [row] [t] (_ : show t) name (f : $row -> t) : colMeta row computedState =
321 Display = fn x => x, 338 Display = fn x => x,
322 Edit = fn _ => <xml>...</xml>, 339 Edit = fn _ => <xml>...</xml>,
323 Validate = fn _ => return True, 340 Validate = fn _ => return True,
324 CreateFilter = return (), 341 CreateFilter = return (),
325 DisplayFilter = fn _ => <xml/>, 342 DisplayFilter = fn _ => <xml/>,
326 Filter = fn _ _ => return True}} 343 Filter = fn _ _ => return True,
344 Sort = None}}
327 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState = 345 fun computedHtml [row] name (f : $row -> xbody) : colMeta row computedState =
328 {Initialize = return (), 346 {Initialize = return (),
329 Handlers = fn () => {Header = name, 347 Handlers = fn () => {Header = name,
330 Project = fn r => return (f r), 348 Project = fn r => return (f r),
331 Update = fn r _ => return r, 349 Update = fn r _ => return r,
332 Display = fn x => x, 350 Display = fn x => x,
333 Edit = fn _ => <xml>...</xml>, 351 Edit = fn _ => <xml>...</xml>,
334 Validate = fn _ => return True, 352 Validate = fn _ => return True,
335 CreateFilter = return (), 353 CreateFilter = return (),
336 DisplayFilter = fn _ => <xml/>, 354 DisplayFilter = fn _ => <xml/>,
337 Filter = fn _ _ => return True}} 355 Filter = fn _ _ => return True,
356 Sort = None}}
338 357
339 functor Make(M : sig 358 functor Make(M : sig
340 con key :: {Type} 359 con key :: {Type}
341 con row :: {Type} 360 con row :: {Type}
342 constraint key ~ row 361 constraint key ~ row