# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1311533476 14400
# Node ID ccd0a169e8277f92acedbe0b6d9e82ae521adf8f
# Parent  0337f88f2efc392f13b34a302b7a07b2833be2b1
Clock corrects for skew, so that it matches server time (if an RPC round-trips fast enough)

diff -r 0337f88f2efc -r ccd0a169e827 clock.ur
--- 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