Ur/Web: demo/more/expandable.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	7facf72aaf0a
children

rev	line source
adamc@1025	1 con t ctx = source bool * xml ctx [] []
adamc@1025	2
adamc@1025	3 fun create [ctx] (x : xml ctx [] []) =
adamc@1025	4 s <- source False;
adamc@1025	5 return (s, x)
adamc@1025	6
adamc@1025	7 fun expand [ctx] (t : t ctx) =
adamc@1025	8 set t.1 True
adamc@1025	9
adamc@1025	10 fun collapse [ctx] (t : t ctx) =
adamc@1025	11 set t.1 False
adamc@1025	12
adamc@1025	13 fun render [ctx] [[Body] ~ ctx] (t : t ([Body] ++ ctx)) =
adamc@1025	14 <xml><dyn signal={b <- signal t.1;
adamc@1025	15 return (if b then
adamc@1025	16 <xml>
adamc@1025	17 <button value="-" onclick={collapse t}/><br/>
adamc@1025	18 {t.2}
adamc@1025	19 </xml>
adamc@1025	20 else
adamc@1025	21 <xml>
adamc@1025	22 <button value="+" onclick={expand t}/><br/>
adamc@1025	23 </xml>)}/></xml>

Mercurial > urweb