comparison demo/more/dlist.ur @ 957:2831be2daf2e

Grid changed to use Dlist.replace; filters stopped working
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Sep 2009 19:01:04 -0400
parents 2a50da66ffd8
children 3aaac251a5af
comparison
equal deleted inserted replaced
956:d80734855790 957:2831be2daf2e
56 let 56 let
57 fun build ls acc = 57 fun build ls acc =
58 case ls of 58 case ls of
59 [] => return acc 59 [] => return acc
60 | x :: ls => 60 | x :: ls =>
61 this <- source (Cons (x, tl)); 61 this <- source (Cons (x, acc));
62 build ls this 62 build ls this
63 in 63 in
64 hd <- build (List.rev ls) tl; 64 hd <- build (List.rev ls) tl;
65 tlS <- source tl; 65 tlS <- source tl;
66 set dl (Nonempty {Head = Cons (x, hd), Tail = tlS}) 66 set dl (Nonempty {Head = Cons (x, hd), Tail = tlS})