changeset 11:ccd0a169e827

Clock corrects for skew, so that it matches server time (if an RPC round-trips fast enough)
author Adam Chlipala <adam@chlipala.net>
date Sun, 24 Jul 2011 14:51:16 -0400
parents 0337f88f2efc
children bbdedfde154e
files clock.ur
diffstat 1 files changed, 14 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/clock.ur	Fri Jul 22 15:40:03 2011 -0400
+++ b/clock.ur	Sun Jul 24 14:51:16 2011 -0400
@@ -1,21 +1,31 @@
 (** Reactive view of the current time *)
 
-type t = { Source : source time,
-           Period : int }
+type t = {
+     Source : source time, (* Server time as of last tick event *)
+     Skew : source int,    (* How many seconds do we add to the local clock to match the server clock? *)
+     Period : int          (* How many milliseconds between ticks? *)
+}
 
 fun create ms =
     tm <- now;
     t <- source tm;
-    return {Source = t, Period = ms}
+    sk <- source 0;
+    return {Source = t, Skew = sk, Period = ms}
 
 fun start t =
     let
         fun loop () =
             sleep t.Period;
             tm <- now;
-            set t.Source tm;
+            sk <- get t.Skew;
+            set t.Source (addSeconds tm sk);
             loop ()
+
+        fun serverTime () = now
     in
+        spawn (server <- rpc (serverTime ());
+               local <- now;
+               set t.Skew (diffInSeconds server local));
         spawn (loop ())
     end