aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:21:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-19 14:21:25 -0400
commit142e0b28763660019a6fc0fc4a9383fb43b77407 (patch)
tree0f7d66a99a62a66dbf3199febbcac8be00eb0650 /demo
parentc9c3eaa4c489077ef0199eacc16674b328348734 (diff)
Paging mostly working; just need to get it working properly with filtering
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dbgrid.ur4
-rw-r--r--demo/more/dbgrid.urs2
-rw-r--r--demo/more/dlist.ur14
-rw-r--r--demo/more/dlist.urs1
-rw-r--r--demo/more/grid.ur49
-rw-r--r--demo/more/grid.urs2
-rw-r--r--demo/more/grid1.ur2
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 () =