Mercurial > urweb
comparison demo/more/dlist.ur @ 952:07569af40069
Insert dummy Sort parameter
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 17 Sep 2009 14:42:02 -0400 |
parents | 103ac1792c41 |
children | 301530da2062 |
comparison
equal
deleted
inserted
replaced
951:103ac1792c41 | 952:07569af40069 |
---|---|
46 new <- source Nil; | 46 new <- source Nil; |
47 set cur (Cons (v, new)); | 47 set cur (Cons (v, new)); |
48 set tl new; | 48 set tl new; |
49 return (tailPos cur new tl) | 49 return (tailPos cur new tl) |
50 | 50 |
51 fun render [ctx] [ctx ~ body] [t] f {Filter = filter, ...} dl = <xml> | 51 fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter dl = <xml> |
52 <dyn signal={dl' <- signal dl; | 52 <dyn signal={dl' <- signal dl; |
53 return (case dl' of | 53 return (case dl' of |
54 Empty => <xml/> | 54 Empty => <xml/> |
55 | Nonempty {Head = hd, Tail = tlTop} => | 55 | Nonempty {Head = hd, Tail = tlTop} => |
56 let | 56 let |
73 end | 73 end |
74 in | 74 in |
75 render' None hd | 75 render' None hd |
76 end)}/> | 76 end)}/> |
77 </xml> | 77 </xml> |
78 | |
79 fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter ls = | |
80 List.mapX (fn p => f p.1 p.2) ls | |
81 | |
82 fun render [ctx] [ctx ~ body] [t] f r dl = <xml> | |
83 <dyn signal={sort <- r.Sort; | |
84 case sort of | |
85 None => return (renderDyn f r.Filter dl) | |
86 | Some sort => | |
87 dl' <- signal dl; | |
88 elems <- (case dl' of | |
89 Empty => return [] | |
90 | Nonempty {Head = hd, Tail = tlTop} => | |
91 let | |
92 fun listOut prev dl'' acc = | |
93 case dl'' of | |
94 Nil => return acc | |
95 | Cons (v, tl) => | |
96 let | |
97 val pos = case prev of | |
98 None => headPos dl | |
99 | Some prev => tailPos prev tl tlTop | |
100 in | |
101 tl' <- signal tl; | |
102 listOut (Some tl) tl' ((v, pos) :: acc) | |
103 end | |
104 in | |
105 listOut None hd [] | |
106 end); | |
107 return (renderFlat f r.Filter elems)}/> | |
108 </xml> | |
109 | |
110 | |
78 | 111 |
79 fun delete pos = pos | 112 fun delete pos = pos |
80 | 113 |
81 fun elements' [t] (dl'' : dlist'' t) = | 114 fun elements' [t] (dl'' : dlist'' t) = |
82 case dl'' of | 115 case dl'' of |