annotate demo/listEdit.ur @ 1218:48d2ca496d2c

Path conditions, used to track implicit flows
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 13:02:15 -0400
parents fb2a0e76dcef
children e6bc6bbd7a32
rev   line source
adamc@646 1 datatype rlist = Nil | Cons of {Data : source string,
adamc@646 2 NewData : source string,
adamc@646 3 Tail : source rlist}
adamc@646 4
adamc@646 5 fun showString ss =
adamc@646 6 s <- signal ss;
adamc@646 7 return <xml>{[s]}</xml>
adamc@646 8
adamc@646 9 fun show rls =
adamc@646 10 v <- signal rls;
adamc@646 11 show' v
adamc@646 12
adamc@646 13 and show' rl =
adamc@646 14 case rl of
adamc@646 15 Nil => return <xml/>
adamc@646 16 | Cons {Data = ss, NewData = ss', Tail = rls} => return <xml>
adamc@646 17 <dyn signal={showString ss}/>
adamc@646 18 <button value="Change to:" onclick={s <- get ss'; set ss s}/>
adamc@646 19 <ctextbox source={ss'}/><br/>
adamc@646 20 <dyn signal={show rls}/>
adamc@646 21 </xml>
adamc@646 22
adamc@646 23 fun main () =
adamc@646 24 head <- source Nil;
adamc@646 25 tailP <- source head;
adamc@646 26 data <- source "";
adamc@646 27
adamc@646 28 let
adamc@646 29 fun add () =
adamc@646 30 data <- get data;
adamc@646 31 data <- source data;
adamc@646 32 ndata <- source "";
adamc@646 33 tail <- get tailP;
adamc@646 34 tail' <- source Nil;
adamc@646 35
adamc@646 36 let
adamc@646 37 val cons = Cons {Data = data, NewData = ndata, Tail = tail'}
adamc@646 38 in
adamc@646 39 set tail cons;
adamc@646 40 set tailP tail';
adamc@646 41
adamc@646 42 head' <- get head;
adamc@646 43 case head' of
adamc@646 44 Nil => set head cons
adamc@646 45 | _ => return ()
adamc@646 46 end
adamc@646 47 in
adamc@646 48 return <xml><body>
adamc@646 49 <ctextbox source={data}/> <button value="Add" onclick={add ()}/><br/>
adamc@646 50 <br/>
adamc@646 51
adamc@646 52 <dyn signal={show head}/>
adamc@646 53 </body></xml>
adamc@646 54 end