annotate tests/chat.ur @ 1667:833402503855

Tweak Especialize heuristic to prevent non-termination
author Adam Chlipala <adam@chlipala.net>
date Mon, 09 Jan 2012 09:51:39 -0500
parents 01b6f2ee2ef0
children
rev   line source
adamc@679 1 datatype log = End | Line of string * source log
adamc@679 2
adamc@679 3 fun render log =
adamc@679 4 case log of
adamc@679 5 End => <xml/>
adamc@679 6 | Line (line, logS) => <xml>{[line]}<br/><dyn signal={renderS logS}/></xml>
adamc@679 7
adamc@679 8 and renderS logS =
adamc@679 9 log <- signal logS;
adamc@679 10 return (render log)
adamc@679 11
adamc@682 12 structure Room = Broadcast(struct
adamc@682 13 type t = string
adamc@682 14 end)
adamc@682 15
adamc@678 16 sequence s
adamc@682 17 table t : { Id : int, Title : string, Room : Room.topic }
adamc@678 18
adamc@679 19 fun chat id =
adamc@682 20 r <- oneRow (SELECT t.Title, t.Room FROM t WHERE t.Id = {[id]});
adamc@682 21 ch <- Room.subscribe r.T.Room;
adamc@679 22
adamc@679 23 newLine <- source "";
adamc@679 24 logHead <- source End;
adamc@679 25 logTail <- source logHead;
adamc@679 26
adamc@679 27 let
adamc@679 28 fun onload () =
adamc@679 29 let
adamc@679 30 fun listener () =
adamc@679 31 s <- recv ch;
adamc@679 32 oldTail <- get logTail;
adamc@679 33 newTail <- source End;
adamc@679 34 set oldTail (Line (s, newTail));
adamc@679 35 set logTail newTail;
adamc@679 36 listener ()
adamc@679 37 in
adamc@679 38 listener ()
adamc@679 39 end
adamc@679 40
adamc@682 41 fun getRoom () =
adamc@682 42 r <- oneRow (SELECT t.Room FROM t WHERE t.Id = {[id]});
adamc@682 43 return r.T.Room
adamc@682 44
adamc@679 45 fun speak line =
adamc@682 46 room <- getRoom ();
adamc@682 47 Room.send room line
adamc@679 48
adamc@679 49 fun doSpeak () =
adamc@679 50 line <- get newLine;
adamc@690 51 set newLine "";
adamc@679 52 speak line
adamc@679 53 in
adamc@679 54 return <xml><body onload={onload ()}>
adamc@679 55 <h1>{[r.T.Title]}</h1>
adamc@679 56
adamc@679 57 <button value="Send:" onclick={doSpeak ()}/> <ctextbox source={newLine}/>
adamc@679 58
adamc@679 59 <h2>Messages</h2>
adamc@679 60
adamc@679 61 <dyn signal={renderS logHead}/>
adamc@679 62
adamc@679 63 </body></xml>
adamc@679 64 end
adamc@679 65
adamc@678 66 fun list () =
adamc@678 67 queryX (SELECT * FROM t)
adamc@678 68 (fn r => <xml><tr>
adamc@679 69 <td>{[r.T.Id]}</td> <td><a link={chat r.T.Id}>{[r.T.Title]}</a></td>
adamc@678 70 <td><a link={delete r.T.Id}>[delete]</a></td>
adamc@678 71 </tr></xml>)
adamc@678 72
adamc@678 73 and delete id =
adamc@678 74 dml (DELETE FROM t WHERE Id = {[id]});
adamc@678 75 main ()
adamc@678 76
adamc@678 77 and main () : transaction page =
adamc@678 78 let
adamc@678 79 fun create r =
adamc@678 80 id <- nextval s;
adamc@682 81 room <- Room.create;
adamc@682 82 dml (INSERT INTO t (Id, Title, Room) VALUES ({[id]}, {[r.Title]}, {[room]}));
adamc@678 83 main ()
adamc@678 84 in
adamc@678 85 ls <- list ();
adamc@678 86 return <xml><body>
adamc@678 87 <table>
adamc@678 88 <tr> <th>ID</th> <th>Title</th> </tr>
adamc@678 89 {ls}
adamc@678 90 </table>
adamc@678 91
adamc@678 92 <h1>New Channel</h1>
adamc@678 93
adamc@678 94 <form>
adamc@678 95 Title: <textbox{#Title}/><br/>
adamc@678 96 <submit action={create}/>
adamc@678 97 </form>
adamc@678 98 </body></xml>
adamc@678 99 end