diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-09-17 14:42:02 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-17 14:42:02 -0400 |
commit | a8f7c10142c355dbf032c0f3ba7a1e96d53b9039 (patch) | |
tree | 20e527095124269a793c3f4e8df50358ee5e7314 /demo/more | |
parent | db724bd8cdb5cc0627171ab25db2b05a82554ad3 (diff) |
Insert dummy Sort parameter
Diffstat (limited to 'demo/more')
-rw-r--r-- | demo/more/dlist.ur | 35 | ||||
-rw-r--r-- | demo/more/dlist.urs | 3 | ||||
-rw-r--r-- | demo/more/grid.ur | 3 |
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] |