annotate waitbox.ur @ 27:5905b56e0cd9

Adapt to new HTML contexts
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Dec 2011 21:04:21 -0500
parents 37eefd0a2ed4
children
rev   line source
adam@0 1 type t = {Milliseconds : int,
adam@0 2 Action : source (string -> transaction {}),
adam@0 3 Timer : source (option Timer.t),
adam@0 4 Text : source string}
adam@0 5
adam@0 6 fun create n =
adam@0 7 s <- source "";
adam@0 8 tmO <- source None;
adam@0 9 f <- source (fn _ => return ());
adam@0 10
adam@0 11 return {Milliseconds = n, Action = f, Timer = tmO, Text = s}
adam@0 12
adam@0 13 fun setAction r v = set r.Action v
adam@0 14
adam@0 15 fun tickle r =
adam@0 16 last <- get r.Timer;
adam@0 17 (case last of
adam@0 18 None => return ()
adam@0 19 | Some tm => Timer.cancel tm);
adam@0 20 tm <- Timer.create {Milliseconds = r.Milliseconds,
adam@0 21 Action = (set r.Timer None;
adam@0 22 s <- get r.Text;
adam@0 23 f <- get r.Action;
adam@0 24 f s)};
adam@0 25 set r.Timer (Some tm)
adam@0 26
adam@0 27 fun render r = <xml>
adam@0 28 <ctextbox source={r.Text}
adam@0 29 onkeyup={fn _ => tickle r}/>
adam@0 30 </xml>
adam@0 31
adam@0 32 fun clear r = (set r.Text "";
adam@0 33 tm <- get r.Timer;
adam@0 34 (case tm of
adam@0 35 None => return ()
adam@0 36 | Some tm => Timer.cancel tm);
adam@0 37 set r.Timer None)
adam@0 38
adam@0 39 fun trigger r =
adam@0 40 last <- get r.Timer;
adam@0 41 (case last of
adam@0 42 None => return ()
adam@0 43 | Some tm => Timer.cancel tm);
adam@0 44 set r.Timer None;
adam@0 45 s <- get r.Text;
adam@0 46 f <- get r.Action;
adam@0 47 f s