diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 14:21:25 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-19 14:21:25 -0400 |
commit | 19c729dcf5854c528053d71a9c9c38d01d2ac923 (patch) | |
tree | 0f7d66a99a62a66dbf3199febbcac8be00eb0650 /demo | |
parent | ea30827e1977b1d1d028aa7701519bf95b976a3a (diff) |
Paging mostly working; just need to get it working properly with filtering
Diffstat (limited to 'demo')
-rw-r--r-- | demo/more/dbgrid.ur | 4 | ||||
-rw-r--r-- | demo/more/dbgrid.urs | 2 | ||||
-rw-r--r-- | demo/more/dlist.ur | 14 | ||||
-rw-r--r-- | demo/more/dlist.urs | 1 | ||||
-rw-r--r-- | demo/more/grid.ur | 49 | ||||
-rw-r--r-- | demo/more/grid.urs | 2 | ||||
-rw-r--r-- | demo/more/grid1.ur | 2 |
7 files changed, 70 insertions, 4 deletions
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur index a935e900..fe77f21b 100644 --- a/demo/more/dbgrid.ur +++ b/demo/more/dbgrid.ur @@ -373,6 +373,8 @@ functor Make(M : sig 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 @@ functor Make(M : sig val aggregates = M.aggregates val aggFolder = M.aggFolder + + val pageLength = M.pageLength end) end diff --git a/demo/more/dbgrid.urs b/demo/more/dbgrid.urs index f241c334..7dfd3db3 100644 --- a/demo/more/dbgrid.urs +++ b/demo/more/dbgrid.urs @@ -118,6 +118,8 @@ functor Make(M : sig con aggregates :: {Type} val aggregates : $(map (aggregateMeta (key ++ row)) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) : sig type grid diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur index 1a5be7e3..fe0cdd07 100644 --- a/demo/more/dlist.ur +++ b/demo/more/dlist.ur @@ -246,6 +246,20 @@ fun elements [t] (dl : dlist t) = 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 = diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs index 4da61863..6918fdc8 100644 --- a/demo/more/dlist.urs +++ b/demo/more/dlist.urs @@ -8,6 +8,7 @@ val replace : t ::: Type -> dlist t -> list t -> transaction unit 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 diff --git a/demo/more/grid.ur b/demo/more/grid.ur index 560ff146..d63a1424 100644 --- a/demo/more/grid.ur +++ b/demo/more/grid.ur @@ -37,6 +37,8 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig 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 @@ functor Make(M : sig [_] 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 @@ functor Make(M : sig [_] 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}/> diff --git a/demo/more/grid.urs b/demo/more/grid.urs index 30cd9bc6..a918c67b 100644 --- a/demo/more/grid.urs +++ b/demo/more/grid.urs @@ -37,6 +37,8 @@ functor Make(M : sig con aggregates :: {Type} val aggregates : $(map (aggregateMeta row) aggregates) val aggFolder : folder aggregates + + val pageLength : option int end) : sig type grid diff --git a/demo/more/grid1.ur b/demo/more/grid1.ur index c163c9d5..1eb5e596 100644 --- a/demo/more/grid1.ur +++ b/demo/more/grid1.ur @@ -57,6 +57,8 @@ open Make(struct And = {Initial = True, Step = fn r b => r.C && b, Display = txt}} + + val pageLength = Some 10 end) fun main () = |