Mercurial > urweb

annotate demo/more/grid.ur @ 1120:74f2eb3b0606

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis.debug; more restrictive type for Basis.form; weaken definition of polymorphic-ness for especialization
author Adam Chlipala <adamc@hcoop.net>
date Thu, 07 Jan 2010 14:02:58 -0500
parents 8d3aa6c7cee0
children ad15700272f6
rev   line source
adamc@944 1 con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
adamc@915 2 {Header : string,
adamc@944 3 Project : row -> transaction input,
adamc@944 4 Update : row -> input -> transaction row,
adamc@944 5 Display : input -> xbody,
adamc@944 6 Edit : input -> xbody,
adamc@944 7 Validate : input -> signal bool,
adamc@944 8 CreateFilter : transaction filter,
adamc@944 9 DisplayFilter : filter -> xbody,
adamc@961 10 Filter : filter -> row -> signal bool,
adamc@961 11 Sort : option (row -> row -> bool)}
adamc@1002 12
adamc@1002 13 con colMeta = fn (row :: Type) (global :: Type, input :: Type, filter :: Type) =>
adamc@1002 14 {Initialize : transaction global,
adamc@1002 15 Handlers : global -> colMeta' row input filter}
adamc@915 16
adamc@935 17 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
adamc@935 18 {Initial : acc,
adamc@935 19 Step : row -> acc -> acc,
adamc@935 20 Display : acc -> xbody}
adamc@935 21
adamc@915 22 functor Make(M : sig
adamc@915 23 type row
adamc@936 24 type key
adamc@936 25 val keyOf : row -> key
adamc@936 26
adamc@915 27 val list : transaction (list row)
adamc@915 28 val new : transaction row
adamc@936 29 val save : key -> row -> transaction unit
adamc@936 30 val delete : key -> transaction unit
adamc@915 31
adamc@944 32 con cols :: {(Type * Type * Type)}
adamc@915 33 val cols : $(map (colMeta row) cols)
adamc@915 34
adamc@915 35 val folder : folder cols
adamc@935 36
adamc@935 37 con aggregates :: {Type}
adamc@935 38 val aggregates : $(map (aggregateMeta row) aggregates)
adamc@937 39 val aggFolder : folder aggregates
adamc@964 40
adamc@964 41 val pageLength : option int
adamc@915 42 end) = struct
adamc@915 43 style tabl
adamc@915 44 style tr
adamc@915 45 style th
adamc@915 46 style td
adamc@937 47 style agg
adamc@915 48
adamc@944 49 fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
adamc@915 50
adamc@944 51 fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
adamc@1093 52 (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
adamc@1093 53 (fn [p] data meta => make row(meta.Handlers data))
adamc@1093 54 M.folder cols M.cols)
adamc@915 55 (@@Folder.mp [_] [_] M.folder)
adamc@915 56
adamc@944 57 type grid = {Cols : $(map fst3 M.cols),
adamc@940 58 Rows : Dlist.dlist {Row : source M.row,
adamc@944 59 Cols : source ($(map snd3 M.cols)),
adamc@940 60 Updating : source bool,
adamc@940 61 Selected : source bool},
adamc@944 62 Selection : source bool,
adamc@960 63 Filters : $(map thd3 M.cols),
adamc@964 64 Sort : source (option (M.row -> M.row -> bool)),
adamc@964 65 Position : source int}
adamc@940 66
adamc@954 67 fun newRow cols row =
adamc@915 68 rowS <- source row;
adamc@915 69 cols <- makeAll cols row;
adamc@915 70 colsS <- source cols;
adamc@915 71 ud <- source False;
adamc@940 72 sd <- source False;
adamc@954 73 return {Row = rowS,
adamc@954 74 Cols = colsS,
adamc@954 75 Updating = ud,
adamc@954 76 Selected = sd}
adamc@954 77
adamc@954 78 fun addRow cols rows row =
adamc@954 79 r <- newRow cols row;
adamc@954 80 Monad.ignore (Dlist.append rows r)
adamc@915 81
adamc@944 82 val grid =
adamc@1093 83 cols <- @Monad.mapR _ [colMeta M.row] [fst3]
adamc@1093 84 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
adamc@1093 85 M.folder M.cols;
adamc@915 86
adamc@1093 87 filters <- @Monad.mapR2 _ [colMeta M.row] [fst3] [thd3]
adamc@1093 88 (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
adamc@1093 89 (meta.Handlers state).CreateFilter)
adamc@1093 90 M.folder M.cols cols;
adamc@944 91
adamc@951 92 rows <- Dlist.create;
adamc@940 93 sel <- source False;
adamc@960 94 sort <- source None;
adamc@964 95 pos <- source 0;
adamc@951 96
adamc@951 97 return {Cols = cols,
adamc@951 98 Rows = rows,
adamc@951 99 Selection = sel,
adamc@960 100 Filters = filters,
adamc@964 101 Sort = sort,
adamc@964 102 Position = pos}
adamc@915 103
adamc@940 104 fun sync {Cols = cols, Rows = rows, ...} =
adamc@915 105 Dlist.clear rows;
adamc@915 106 init <- rpc M.list;
adamc@954 107 rs <- List.mapM (newRow cols) init;
adamc@954 108 Dlist.replace rows rs
adamc@915 109
adamc@965 110 fun myFilter grid all =
adamc@965 111 row <- signal all.Row;
adamc@1093 112 @foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
adamc@1093 113 (fn [nm :: Name] [p :: (Type * Type * Type)]
adamc@1093 114 [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@1093 115 meta state filter combinedFilter row =>
adamc@1093 116 previous <- combinedFilter row;
adamc@1093 117 this <- (meta.Handlers state).Filter filter row;
adamc@1093 118 return (previous && this))
adamc@1093 119 (fn _ => return True)
adamc@1093 120 M.folder M.cols grid.Cols grid.Filters row
adamc@965 121
adamc@961 122 fun render (grid : grid) = <xml>
adamc@915 123 <table class={tabl}>
adamc@915 124 <tr class={tr}>
adamc@961 125 <th/> <th/> <th><button value="No sort" onclick={set grid.Sort None}/></th>
adamc@1093 126 {@foldRX2 [fst3] [colMeta M.row] [_]
adamc@1093 127 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@1093 128 data (meta : colMeta M.row p) =>
adamc@1093 129 <xml><th class={th}>
adamc@1093 130 {case (meta.Handlers data).Sort of
adamc@1093 131 None => txt (meta.Handlers data).Header
adamc@1093 132 | sort => <xml><button value={(meta.Handlers data).Header}
adamc@1093 133 onclick={set grid.Sort sort}/></xml>}
adamc@1093 134 </th></xml>)
adamc@1093 135 M.folder grid.Cols M.cols}
adamc@937 136 </tr>
adamc@915 137
adamc@940 138 {Dlist.render (fn {Row = rowS, Cols = colsS, Updating = ud, Selected = sd} pos =>
adamc@937 139 let
adamc@937 140 val delete =
adamc@937 141 Dlist.delete pos;
adamc@937 142 row <- get rowS;
adamc@937 143 rpc (M.delete (M.keyOf row))
adamc@915 144
adamc@937 145 val update = set ud True
adamc@915 146
adamc@937 147 val cancel =
adamc@937 148 set ud False;
adamc@937 149 row <- get rowS;
adamc@937 150 cols <- makeAll grid.Cols row;
adamc@937 151 set colsS cols
adamc@937 152
adamc@937 153 val save =
adamc@937 154 cols <- get colsS;
adamc@1093 155 errors <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => option string]
adamc@1093 156 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
adamc@1093 157 [[nm] ~ rest] data meta v errors =>
adamc@1093 158 b <- current ((meta.Handlers data).Validate v);
adamc@1093 159 return (if b then
adamc@1093 160 errors
adamc@1093 161 else
adamc@1093 162 case errors of
adamc@1093 163 None => Some ((meta.Handlers data).Header)
adamc@1093 164 | Some s => Some ((meta.Handlers data).Header
adamc@1093 165 ^ ", " ^ s)))
adamc@1093 166 None M.folder grid.Cols M.cols cols;
adamc@915 167
adamc@937 168 case errors of
adamc@937 169 Some s => alert ("Can't save because the following columns have invalid values:\n"
adamc@937 170 ^ s)
adamc@937 171 | None =>
adamc@937 172 set ud False;
adamc@937 173 row <- get rowS;
adamc@1093 174 row' <- @Monad.foldR3 _ [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
adamc@1093 175 (fn [nm :: Name] [t :: (Type * Type * Type)]
adamc@1093 176 [rest :: {(Type * Type * Type)}]
adamc@1093 177 [[nm] ~ rest] data meta v row' =>
adamc@1093 178 (meta.Handlers data).Update row' v)
adamc@1093 179 row M.folder grid.Cols M.cols cols;
adamc@937 180 rpc (M.save (M.keyOf row) row');
adamc@937 181 set rowS row';
adamc@937 182
adamc@937 183 cols <- makeAll grid.Cols row';
adamc@937 184 set colsS cols
adamc@937 185 in
adamc@937 186 <xml><tr class={tr}>
adamc@937 187 <td>
adamc@940 188 <dyn signal={b <- signal grid.Selection;
adamc@941 189 return (if b then
adamc@940 190 <xml><ccheckbox source={sd}/></xml>
adamc@940 191 else
adamc@941 192 <xml/>)}/>
adamc@940 193 </td>
adamc@940 194
adamc@940 195 <td>
adamc@937 196 <dyn signal={b <- signal ud;
adamc@937 197 return (if b then
adamc@937 198 <xml><button value="Save" onclick={save}/></xml>
adamc@937 199 else
adamc@937 200 <xml><button value="Update" onclick={update}/></xml>)}/>
adamc@937 201 </td>
adamc@937 202
adamc@937 203 <td><dyn signal={b <- signal ud;
adamc@937 204 return (if b then
adamc@937 205 <xml><button value="Cancel" onclick={cancel}/></xml>
adamc@937 206 else
adamc@937 207 <xml><button value="Delete" onclick={delete}/></xml>)}/>
adamc@937 208 </td>
adamc@937 209
adamc@937 210 <dyn signal={cols <- signal colsS;
adamc@1093 211 return (@foldRX3 [fst3] [colMeta M.row] [snd3] [_]
adamc@1093 212 (fn [nm :: Name] [t :: (Type * Type * Type)]
adamc@1093 213 [rest :: {(Type * Type * Type)}]
adamc@1093 214 [[nm] ~ rest] data meta v =>
adamc@1093 215 <xml><td class={td}>
adamc@1093 216 <dyn signal={b <- signal ud;
adamc@1093 217 return (if b then
adamc@1093 218 (meta.Handlers data).Edit v
adamc@1093 219 else
adamc@1093 220 (meta.Handlers data).Display
adamc@1093 221 v)}/>
adamc@1093 222 <dyn signal={b <- signal ud;
adamc@1093 223 if b then
adamc@1093 224 valid <-
adamc@1093 225 (meta.Handlers data).Validate v;
adamc@1093 226 return (if valid then
adamc@1093 227 <xml/>
adamc@1093 228 else
adamc@1093 229 <xml>!</xml>)
adamc@1093 230 else
adamc@1093 231 return <xml/>}/>
adamc@1093 232 </td></xml>)
adamc@1093 233 M.folder grid.Cols M.cols cols)}/>
adamc@937 234 </tr></xml>
adamc@951 235 end)
adamc@965 236 {StartPosition = case M.pageLength of
adamc@965 237 None => return None
adamc@965 238 | Some len =>
adamc@965 239 avail <- Dlist.numPassing (myFilter grid) grid.Rows;
adamc@965 240 pos <- signal grid.Position;
adamc@965 241 return (Some (if pos >= avail then
adamc@965 242 0
adamc@965 243 else
adamc@965 244 pos)),
adamc@964 245 MaxLength = return M.pageLength,
adamc@965 246 Filter = myFilter grid,
adamc@960 247 Sort = f <- signal grid.Sort;
adamc@960 248 return (Option.mp (fn f r1 r2 => r1 <- signal r1.Row;
adamc@960 249 r2 <- signal r2.Row;
adamc@960 250 return (f r1 r2)) f)}
adamc@951 251 grid.Rows}
adamc@915 252
adamc@1093 253 <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
adamc@1093 254 (fn [nm :: Name] [t :: Type] meta acc =>
adamc@1093 255 Monad.mp (fn v => meta.Step v acc)
adamc@1093 256 (signal row.Row))
adamc@1093 257 M.aggFolder M.aggregates)
adamc@1093 258 (@mp [aggregateMeta M.row] [id]
adamc@937 259 (fn [t] meta => meta.Initial)
adamc@1093 260 M.aggFolder M.aggregates) grid.Rows;
adamc@937 261 return <xml><tr>
adamc@941 262 <th colspan={3}>Aggregates</th>
adamc@1093 263 {@foldRX2 [aggregateMeta M.row] [id] [_]
adamc@1093 264 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
adamc@1093 265 <xml><td class={agg}>{meta.Display acc}</td></xml>)
adamc@1093 266 M.aggFolder M.aggregates rows}
adamc@937 267 </tr></xml>}/>
adamc@944 268
adamc@944 269 <tr><th colspan={3}>Filters</th>
adamc@1093 270 {@foldRX3 [colMeta M.row] [fst3] [thd3] [_]
adamc@1093 271 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@1093 272 meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
adamc@1093 273 M.folder M.cols grid.Cols grid.Filters}
adamc@944 274 </tr>
adamc@915 275 </table>
adamc@964 276
adamc@964 277 {case M.pageLength of
adamc@964 278 None => <xml/>
adamc@964 279 | Some plen => <xml>
adamc@965 280 <dyn signal={avail <- Dlist.numPassing (myFilter grid) grid.Rows;
adamc@964 281 return (if avail <= plen then
adamc@964 282 <xml/>
adamc@964 283 else
adamc@964 284 let
adamc@964 285 val numPages = avail / plen
adamc@964 286 val numPages = if numPages * plen < avail then
adamc@964 287 numPages + 1
adamc@964 288 else
adamc@964 289 numPages
adamc@964 290
adamc@964 291 fun pages n =
adamc@964 292 if n * plen >= avail then
adamc@964 293 <xml/>
adamc@964 294 else
adamc@964 295 <xml>
adamc@964 296 <dyn signal={pos <- signal grid.Position;
adamc@964 297 return (if n * plen = pos then
adamc@964 298 <xml><b>{[n + 1]}</b></xml>
adamc@964 299 else
adamc@964 300 <xml>
adamc@964 301 <button value={show (n + 1)}
adamc@964 302 onclick={set grid.Position
adamc@964 303 (n * plen)
adamc@964 304 }/></xml>)}/>
adamc@964 305 {if (n + 1) * plen >= avail then <xml/> else <xml>|</xml>}
adamc@964 306 {pages (n + 1)}
adamc@964 307 </xml>
adamc@964 308 in
adamc@964 309 <xml><p><b>Pages:</b> {pages 0}</p></xml>
adamc@964 310 end)}/>
adamc@964 311 </xml>}
adamc@915 312
adamc@915 313 <button value="New row" onclick={row <- rpc M.new;
adamc@915 314 addRow grid.Cols grid.Rows row}/>
adamc@915 315 <button value="Refresh" onclick={sync grid}/>
adamc@915 316 </xml>
adamc@940 317
adamc@940 318 fun showSelection grid = grid.Selection
adamc@940 319
adamc@940 320 fun selection grid = Dlist.foldl (fn {Row = rowS, Selected = sd, ...} ls =>
adamc@940 321 sd <- signal sd;
adamc@940 322 if sd then
adamc@940 323 row <- signal rowS;
adamc@940 324 return (row :: ls)
adamc@940 325 else
adamc@940 326 return ls) [] grid.Rows
adamc@915 327 end