Mercurial > urweb
changeset 964:fbc3a0eef45a
Paging mostly working; just need to get it working properly with filtering
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 19 Sep 2009 14:21:25 -0400 |
| parents | 6f9d1565de56 |
| children | e9c5992bc9bc |
| files | demo/more/dbgrid.ur demo/more/dbgrid.urs demo/more/dlist.ur demo/more/dlist.urs demo/more/grid.ur demo/more/grid.urs demo/more/grid1.ur src/urweb.grm |
| diffstat | 8 files changed, 71 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/more/dbgrid.ur Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/dbgrid.ur Sat Sep 19 14:21:25 2009 -0400 @@ -373,6 +373,8 @@ con aggregates :: {Type} val aggregates : $(map (aggregateMeta (key ++ row)) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) = struct open Grid.Make(struct fun keyOf r = r --- M.row @@ -421,5 +423,7 @@ val aggregates = M.aggregates val aggFolder = M.aggFolder + + val pageLength = M.pageLength end) end
--- a/demo/more/dbgrid.urs Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/dbgrid.urs Sat Sep 19 14:21:25 2009 -0400 @@ -118,6 +118,8 @@ con aggregates :: {Type} val aggregates : $(map (aggregateMeta (key ++ row)) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) : sig type grid
--- a/demo/more/dlist.ur Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/dlist.ur Sat Sep 19 14:21:25 2009 -0400 @@ -246,6 +246,20 @@ Empty => return [] | Nonempty {Head = hd, ...} => elements' hd +fun size' [t] (dl'' : dlist'' t) = + case dl'' of + Nil => return 0 + | Cons (x, dl'') => + dl'' <- signal dl''; + n <- size' dl''; + return (n + 1) + +fun size [t] (dl : dlist t) = + dl' <- signal dl; + case dl' of + Empty => return 0 + | Nonempty {Head = hd, ...} => size' hd + fun foldl [t] [acc] (f : t -> acc -> signal acc) = let fun foldl'' (i : acc) (dl : dlist'' t) : signal acc =
--- a/demo/more/dlist.urs Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/dlist.urs Sat Sep 19 14:21:25 2009 -0400 @@ -8,6 +8,7 @@ val delete : position -> transaction unit val elements : t ::: Type -> dlist t -> signal (list t) +val size : t ::: Type -> dlist t -> signal int val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dlist t -> signal acc val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
--- a/demo/more/grid.ur Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/grid.ur Sat Sep 19 14:21:25 2009 -0400 @@ -37,6 +37,8 @@ con aggregates :: {Type} val aggregates : $(map (aggregateMeta row) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) = struct style tabl style tr @@ -59,7 +61,8 @@ Selected : source bool}, Selection : source bool, Filters : $(map thd3 M.cols), - Sort : source (option (M.row -> M.row -> bool))} + Sort : source (option (M.row -> M.row -> bool)), + Position : source int} fun newRow cols row = rowS <- source row; @@ -89,12 +92,14 @@ rows <- Dlist.create; sel <- source False; sort <- source None; + pos <- source 0; return {Cols = cols, Rows = rows, Selection = sel, Filters = filters, - Sort = sort} + Sort = sort, + Position = pos} fun sync {Cols = cols, Rows = rows, ...} = Dlist.clear rows; @@ -216,8 +221,8 @@ [_] M.folder grid.Cols M.cols cols)}/> </tr></xml> end) - {StartPosition = return (Some 1), - MaxLength = return (Some 2), + {StartPosition = Monad.mp Some (signal grid.Position), + MaxLength = return M.pageLength, Filter = fn all => row <- signal all.Row; foldR3 [colMeta M.row] [fst3] [thd3] [fn _ => M.row -> signal bool] @@ -258,6 +263,42 @@ [_] M.folder M.cols grid.Cols grid.Filters} </tr> </table> + + {case M.pageLength of + None => <xml/> + | Some plen => <xml> + <dyn signal={avail <- Dlist.size grid.Rows; + return (if avail <= plen then + <xml/> + else + let + val numPages = avail / plen + val numPages = if numPages * plen < avail then + numPages + 1 + else + numPages + + fun pages n = + if n * plen >= avail then + <xml/> + else + <xml> + <dyn signal={pos <- signal grid.Position; + return (if n * plen = pos then + <xml><b>{[n + 1]}</b></xml> + else + <xml> + <button value={show (n + 1)} + onclick={set grid.Position + (n * plen) + }/></xml>)}/> + {if (n + 1) * plen >= avail then <xml/> else <xml>|</xml>} + {pages (n + 1)} + </xml> + in + <xml><p><b>Pages:</b> {pages 0}</p></xml> + end)}/> + </xml>} <button value="New row" onclick={row <- rpc M.new; addRow grid.Cols grid.Rows row}/>
--- a/demo/more/grid.urs Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/grid.urs Sat Sep 19 14:21:25 2009 -0400 @@ -37,6 +37,8 @@ con aggregates :: {Type} val aggregates : $(map (aggregateMeta row) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) : sig type grid
--- a/demo/more/grid1.ur Sat Sep 19 13:55:37 2009 -0400 +++ b/demo/more/grid1.ur Sat Sep 19 14:21:25 2009 -0400 @@ -57,6 +57,8 @@ And = {Initial = True, Step = fn r b => r.C && b, Display = txt}} + + val pageLength = Some 10 end) fun main () =
--- a/src/urweb.grm Sat Sep 19 13:55:37 2009 -0400 +++ b/src/urweb.grm Sat Sep 19 14:21:25 2009 -0400 @@ -938,7 +938,7 @@ | eexp PLUS eexp (native_op ("plus", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp MINUS eexp (native_op ("minus", eexp1, eexp2, s (eexp1left, eexp2right))) | eterm STAR eexp (native_op ("times", eterm, eexp, s (etermleft, eexpright))) - | eexp DIVIDE eexp (native_op ("div", eexp1, eexp2, s (eexp1left, eexp2right))) + | eexp DIVIDE eexp (native_op ("divide", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp MOD eexp (native_op ("mod", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp LT eexp (native_op ("lt", eexp1, eexp2, s (eexp1left, eexp2right)))