Mercurial > urweb
comparison demo/more/dlist.ur @ 915:5e8b6fa5b48f
Start 'more' demo with dbgrid
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 08 Sep 2009 07:48:57 -0400 |
parents | |
children | 37dd42935dad |
comparison
equal
deleted
inserted
replaced
914:782f0b4eea67 | 915:5e8b6fa5b48f |
---|---|
1 datatype dlist'' t = | |
2 Nil | |
3 | Cons of t * source (dlist'' t) | |
4 | |
5 datatype dlist' t = | |
6 Empty | |
7 | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) } | |
8 | |
9 con dlist t = source (dlist' t) | |
10 | |
11 type position = transaction unit | |
12 | |
13 fun headPos [t] (dl : dlist t) = | |
14 dl' <- get dl; | |
15 case dl' of | |
16 Nonempty { Head = Cons (_, tl), Tail = tl' } => | |
17 cur <- get tl; | |
18 set dl (case cur of | |
19 Nil => Empty | |
20 | _ => Nonempty {Head = cur, Tail = tl'}) | |
21 | _ => return () | |
22 | |
23 fun tailPos [t] (cur : source (dlist'' t)) new tail = | |
24 new' <- get new; | |
25 set cur new'; | |
26 | |
27 case new' of | |
28 Nil => set tail cur | |
29 | _ => return () | |
30 | |
31 val create = fn [t] => source Empty | |
32 | |
33 fun clear [t] (s : dlist t) = set s Empty | |
34 | |
35 fun append [t] dl v = | |
36 dl' <- get dl; | |
37 case dl' of | |
38 Empty => | |
39 tl <- source Nil; | |
40 tl' <- source tl; | |
41 set dl (Nonempty {Head = Cons (v, tl), Tail = tl'}); | |
42 return (headPos dl) | |
43 | |
44 | Nonempty {Tail = tl, ...} => | |
45 cur <- get tl; | |
46 new <- source Nil; | |
47 set cur (Cons (v, new)); | |
48 set tl new; | |
49 return (tailPos cur new tl) | |
50 | |
51 fun render [ctx] [ctx ~ body] [t] f dl = <xml> | |
52 <dyn signal={dl' <- signal dl; | |
53 return (case dl' of | |
54 Empty => <xml/> | |
55 | Nonempty {Head = hd, Tail = tlTop} => | |
56 let | |
57 fun render' prev dl'' = | |
58 case dl'' of | |
59 Nil => <xml/> | |
60 | Cons (v, tl) => | |
61 let | |
62 val pos = case prev of | |
63 None => headPos dl | |
64 | Some prev => tailPos prev tl tlTop | |
65 in | |
66 <xml>{f v pos}<dyn signal={tl' <- signal tl; | |
67 return (render' (Some tl) tl')}/></xml> | |
68 end | |
69 in | |
70 render' None hd | |
71 end)}/> | |
72 </xml> | |
73 | |
74 fun delete pos = pos | |
75 | |
76 fun elements' [t] (dl'' : dlist'' t) = | |
77 case dl'' of | |
78 Nil => return [] | |
79 | Cons (x, dl'') => | |
80 dl'' <- signal dl''; | |
81 tl <- elements' dl''; | |
82 return (x :: tl) | |
83 | |
84 fun elements [t] (dl : dlist t) = | |
85 dl' <- signal dl; | |
86 case dl' of | |
87 Empty => return [] | |
88 | Nonempty {Head = hd, ...} => elements' hd |