Mercurial > urweb

annotate demo/more/grid.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents bb3fc575cfe7
children 8d3aa6c7cee0
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@944 52 (map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
adamc@944 53 (fn [p] data meta => make row [_] [_] (meta.Handlers data))
adamc@915 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@944 83 cols <- Monad.mapR [colMeta M.row] [fst3]
adamc@944 84 (fn [nm :: Name] [p :: (Type * Type * Type)] meta => meta.Initialize)
adamc@944 85 [_] M.folder M.cols;
adamc@915 86
adamc@944 87 filters <- Monad.mapR2 [colMeta M.row] [fst3] [thd3]
adamc@944 88 (fn [nm :: Name] [p :: (Type * Type * Type)] meta state =>
adamc@944 89 (meta.Handlers state).CreateFilter)
adamc@944 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@965 112 foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool]
adamc@965 113 (fn [nm :: Name] [p :: (Type * Type * Type)]
adamc@965 114 [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@965 115 meta state filter combinedFilter row =>
adamc@965 116 previous <- combinedFilter row;
adamc@965 117 this <- (meta.Handlers state).Filter filter row;
adamc@965 118 return (previous && this))
adamc@965 119 (fn _ => return True)
adamc@965 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@944 126 {foldRX2 [fst3] [colMeta M.row] [_]
adamc@944 127 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@937 128 data (meta : colMeta M.row p) =>
adamc@961 129 <xml><th class={th}>
adamc@961 130 {case (meta.Handlers data).Sort of
adamc@961 131 None => txt (meta.Handlers data).Header
adamc@961 132 | sort => <xml><button value={(meta.Handlers data).Header}
adamc@961 133 onclick={set grid.Sort sort}/></xml>}
adamc@961 134 </th></xml>)
adamc@937 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@944 155 errors <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => option string]
adamc@944 156 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}]
adamc@937 157 [[nm] ~ rest] data meta v errors =>
adamc@937 158 b <- current ((meta.Handlers data).Validate v);
adamc@937 159 return (if b then
adamc@937 160 errors
adamc@937 161 else
adamc@937 162 case errors of
adamc@937 163 None => Some ((meta.Handlers data).Header)
adamc@937 164 | Some s => Some ((meta.Handlers data).Header
adamc@937 165 ^ ", " ^ s)))
adamc@937 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@944 174 row' <- Monad.foldR3 [fst3] [colMeta M.row] [snd3] [fn _ => M.row]
adamc@944 175 (fn [nm :: Name] [t :: (Type * Type * Type)]
adamc@944 176 [rest :: {(Type * Type * Type)}]
adamc@937 177 [[nm] ~ rest] data meta v row' =>
adamc@937 178 (meta.Handlers data).Update row' v)
adamc@937 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@944 211 return (foldRX3 [fst3] [colMeta M.row] [snd3] [_]
adamc@944 212 (fn [nm :: Name] [t :: (Type * Type * Type)]
adamc@944 213 [rest :: {(Type * Type * Type)}]
adamc@937 214 [[nm] ~ rest] data meta v =>
adamc@937 215 <xml><td class={td}>
adamc@937 216 <dyn signal={b <- signal ud;
adamc@937 217 return (if b then
adamc@937 218 (meta.Handlers data).Edit v
adamc@937 219 else
adamc@937 220 (meta.Handlers data).Display
adamc@937 221 v)}/>
adamc@937 222 <dyn signal={b <- signal ud;
adamc@937 223 if b then
adamc@937 224 valid <-
adamc@937 225 (meta.Handlers data).Validate v;
adamc@937 226 return (if valid then
adamc@937 227 <xml/>
adamc@937 228 else
adamc@937 229 <xml>!</xml>)
adamc@937 230 else
adamc@937 231 return <xml/>}/>
adamc@937 232 </td></xml>)
adamc@937 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@937 253 <dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id]
adamc@937 254 (fn [nm :: Name] [t :: Type] meta acc =>
adamc@937 255 Monad.mp (fn v => meta.Step v acc)
adamc@937 256 (signal row.Row))
adamc@937 257 [_] M.aggFolder M.aggregates)
adamc@937 258 (mp [aggregateMeta M.row] [id]
adamc@937 259 (fn [t] meta => meta.Initial)
adamc@937 260 [_] M.aggFolder M.aggregates) grid.Rows;
adamc@937 261 return <xml><tr>
adamc@941 262 <th colspan={3}>Aggregates</th>
adamc@937 263 {foldRX2 [aggregateMeta M.row] [id] [_]
adamc@937 264 (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest] meta acc =>
adamc@937 265 <xml><td class={agg}>{meta.Display acc}</td></xml>)
adamc@937 266 [_] M.aggFolder M.aggregates rows}
adamc@937 267 </tr></xml>}/>
adamc@944 268
adamc@944 269 <tr><th colspan={3}>Filters</th>
adamc@944 270 {foldRX3 [colMeta M.row] [fst3] [thd3] [_]
adamc@944 271 (fn [nm :: Name] [p :: (Type * Type * Type)] [rest :: {(Type * Type * Type)}] [[nm] ~ rest]
adamc@944 272 meta state filter => <xml><td>{(meta.Handlers state).DisplayFilter filter}</td></xml>)
adamc@944 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