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 | db87f2d9dd9ef6ea5a9471e13fce81515900e4dc (patch) | |
tree | 20e527095124269a793c3f4e8df50358ee5e7314 /demo/more/dlist.ur | |
parent | e2170d73e8d43842996910a6b512df89e20be389 (diff) |
Insert dummy Sort parameter
Diffstat (limited to 'demo/more/dlist.ur')
-rw-r--r-- | demo/more/dlist.ur | 35 |
1 files changed, 34 insertions, 1 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) = |