# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1253384485 14400
# Node ID fbc3a0eef45ac4acc955f32d58a3aa8abdec6728
# Parent  6f9d1565de56027a19fda69bc31c093c41f56306
Paging mostly working; just need to get it working properly with filtering

diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/dbgrid.ur
--- 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
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/dbgrid.urs
--- 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
 
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/dlist.ur
--- 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 =
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/dlist.urs
--- 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
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/grid.ur
--- 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}/>
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/grid.urs
--- 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
 
diff -r 6f9d1565de56 -r fbc3a0eef45a demo/more/grid1.ur
--- 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 () =
diff -r 6f9d1565de56 -r fbc3a0eef45a src/urweb.grm
--- 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)))