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