aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-09-17 14:42:02 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-09-17 14:42:02 -0400
commitdb87f2d9dd9ef6ea5a9471e13fce81515900e4dc (patch)
tree20e527095124269a793c3f4e8df50358ee5e7314 /demo
parente2170d73e8d43842996910a6b512df89e20be389 (diff)
Insert dummy Sort parameter
Diffstat (limited to 'demo')
-rw-r--r--demo/more/dlist.ur35
-rw-r--r--demo/more/dlist.urs3
-rw-r--r--demo/more/grid.ur3
3 files changed, 38 insertions, 3 deletions
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index a99244ec..244c54a7 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -48,7 +48,7 @@ fun append [t] dl v =
set tl new;
return (tailPos cur new tl)
-fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
+fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter dl = <xml>
<dyn signal={dl' <- signal dl;
return (case dl' of
Empty => <xml/>
@@ -76,6 +76,39 @@ fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml>
end)}/>
</xml>
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls =
+ List.mapX (fn p => f p.1 p.2) ls
+
+fun render [ctx] [ctx ~ body] [t] f r dl = <xml>
+ <dyn signal={sort <- r.Sort;
+ case sort of
+ None => return (renderDyn f r.Filter dl)
+ | Some sort =>
+ dl' <- signal dl;
+ elems <- (case dl' of
+ Empty => return []
+ | Nonempty {Head = hd, Tail = tlTop} =>
+ let
+ fun listOut prev dl'' acc =
+ case dl'' of
+ Nil => return acc
+ | Cons (v, tl) =>
+ let
+ val pos = case prev of
+ None => headPos dl
+ | Some prev => tailPos prev tl tlTop
+ in
+ tl' <- signal tl;
+ listOut (Some tl) tl' ((v, pos) :: acc)
+ end
+ in
+ listOut None hd []
+ end);
+ return (renderFlat f r.Filter elems)}/>
+</xml>
+
+
+
fun delete pos = pos
fun elements' [t] (dl'' : dlist'' t) =
diff --git a/demo/more/dlist.urs b/demo/more/dlist.urs
index a775113e..b912139e 100644
--- a/demo/more/dlist.urs
+++ b/demo/more/dlist.urs
@@ -10,6 +10,7 @@ val foldl : t ::: Type -> acc ::: Type -> (t -> acc -> signal acc) -> acc -> dli
val render : ctx ::: {Unit} -> [ctx ~ body] => t ::: Type
-> (t -> position -> xml (ctx ++ body) [] [])
- -> {Filter : t -> signal bool}
+ -> {Filter : t -> signal bool,
+ Sort : signal (option (t -> t -> signal bool)) (* <= *)}
-> dlist t
-> xml (ctx ++ body) [] []
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index 6dd0543a..a59e1082 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -212,7 +212,8 @@ functor Make(M : sig
this <- (meta.Handlers state).Filter filter row;
return (previous && this))
(fn _ => return True)
- [_] M.folder M.cols grid.Cols grid.Filters row}
+ [_] M.folder M.cols grid.Cols grid.Filters row,
+ Sort = return None}
grid.Rows}
<dyn signal={rows <- Dlist.foldl (fn row => Monad.mapR2 [aggregateMeta M.row] [id] [id]