From 142e0b28763660019a6fc0fc4a9383fb43b77407 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 19 Sep 2009 14:21:25 -0400
Subject: Paging mostly working; just need to get it working properly with
 filtering

---
 demo/more/dbgrid.ur  |  4 ++++
 demo/more/dbgrid.urs |  2 ++
 demo/more/dlist.ur   | 14 ++++++++++++++
 demo/more/dlist.urs  |  1 +
 demo/more/grid.ur    | 49 +++++++++++++++++++++++++++++++++++++++++++++----
 demo/more/grid.urs   |  2 ++
 demo/more/grid1.ur   |  2 ++
 7 files changed, 70 insertions(+), 4 deletions(-)

(limited to 'demo')

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 () =
-- 
cgit v1.2.3