Ur/Web: tests/rpcDO.ur annotate

Hooks for measuring how much interesting proving is going on in elaboration

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 17 Nov 2009 12:44:14 -0500
parents	9da62680adc5
children

rev	line source
adamc@639	1 datatype list t = Nil \| Cons of t * list t
adamc@639	2
adamc@639	3 table t : {A : int}
adamc@639	4
adamc@639	5 fun main () : transaction page =
adamc@639	6 let
adamc@639	7 fun rows () =
adamc@639	8 query (SELECT * FROM t)
adamc@639	9 (fn r ls => return (Cons (r.T.A, ls)))
adamc@639	10 Nil
adamc@639	11
adamc@639	12 fun show ls =
adamc@639	13 case ls of
adamc@639	14 Nil => <xml/>
adamc@639	15 \| Cons (x, ls') => <xml>{[x]}<br/>{show ls'}</xml>
adamc@639	16 in
adamc@639	17 s <- source Nil;
adamc@639	18 return <xml><body>
adamc@639	19 <button value="Get It On!"
adamc@639	20 onclick={ls <- rows ();
adamc@639	21 set s ls}/><br/>
adamc@639	22 <br/>
adamc@639	23 Current: <dyn signal={ls <- signal s; return (show ls)}/>
adamc@639	24 </body></xml>
adamc@639	25 end

Mercurial > urweb