adamc@915: datatype dlist'' t =
adamc@915:          Nil
adamc@915:        | Cons of t * source (dlist'' t)
adamc@915: 
adamc@915: datatype dlist' t =
adamc@915:          Empty
adamc@915:        | Nonempty of { Head : dlist'' t, Tail : source (source (dlist'' t)) }
adamc@915: 
adamc@915: con dlist t = source (dlist' t)
adamc@915: 
adamc@915: type position = transaction unit
adamc@915: 
adamc@915: fun headPos [t] (dl : dlist t) =
adamc@915:     dl' <- get dl;
adamc@915:     case dl' of
adamc@915:         Nonempty { Head = Cons (_, tl), Tail = tl' } =>
adamc@915:         cur <- get tl;
adamc@915:         set dl (case cur of
adamc@915:                     Nil => Empty
adamc@915:                   | _ => Nonempty {Head = cur, Tail = tl'})
adamc@915:       | _ => return ()
adamc@915: 
adamc@915: fun tailPos [t] (cur : source (dlist'' t)) new tail =
adamc@915:     new' <- get new;
adamc@915:     set cur new';
adamc@915: 
adamc@915:     case new' of
adamc@915:         Nil => set tail cur
adamc@915:       | _ => return ()
adamc@915: 
adamc@915: val create = fn [t] => source Empty
adamc@915: 
adamc@915: fun clear [t] (s : dlist t) = set s Empty
adamc@915: 
adamc@915: fun append [t] dl v =
adamc@915:     dl' <- get dl;
adamc@915:     case dl' of
adamc@915:         Empty =>
adamc@915:         tl <- source Nil;
adamc@915:         tl' <- source tl;
adamc@915:         set dl (Nonempty {Head = Cons (v, tl), Tail = tl'});
adamc@915:         return (headPos dl)
adamc@915:                 
adamc@915:       | Nonempty {Tail = tl, ...} =>
adamc@915:         cur <- get tl;
adamc@915:         new <- source Nil;
adamc@915:         set cur (Cons (v, new));
adamc@915:         set tl new;
adamc@915:         return (tailPos cur new tl)
adamc@915: 
adamc@915: fun render [ctx] [ctx ~ body] [t] f dl = <xml>
adamc@915:   <dyn signal={dl' <- signal dl;
adamc@915:                return (case dl' of
adamc@915:                            Empty => <xml/>
adamc@915:                          | Nonempty {Head = hd, Tail = tlTop} => 
adamc@915:                            let
adamc@915:                                fun render' prev dl'' =
adamc@915:                                    case dl'' of
adamc@915:                                        Nil => <xml/>
adamc@915:                                      | Cons (v, tl) =>
adamc@915:                                        let
adamc@915:                                            val pos = case prev of
adamc@915:                                                          None => headPos dl
adamc@915:                                                        | Some prev => tailPos prev tl tlTop
adamc@915:                                        in
adamc@915:                                            <xml>{f v pos}<dyn signal={tl' <- signal tl;
adamc@915:                                                                       return (render' (Some tl) tl')}/></xml>
adamc@915:                                        end
adamc@915:                            in
adamc@915:                                render' None hd
adamc@915:                            end)}/>
adamc@915: </xml>
adamc@915: 
adamc@915: fun delete pos = pos
adamc@915: 
adamc@915: fun elements' [t] (dl'' : dlist'' t) =
adamc@915:     case dl'' of
adamc@915:         Nil => return []
adamc@915:       | Cons (x, dl'') =>
adamc@915:         dl'' <- signal dl'';
adamc@915:         tl <- elements' dl'';
adamc@915:         return (x :: tl)
adamc@915: 
adamc@915: fun elements [t] (dl : dlist t) =
adamc@915:     dl' <- signal dl;
adamc@915:     case dl' of
adamc@915:         Empty => return []
adamc@915:       | Nonempty {Head = hd, ...} => elements' hd