# HG changeset patch
# User wenzelm
# Date 1420891347 -3600
# Node ID abc53a03ca1c56c3c739831f8b85215e7c137deb
# Parent  2ea1bf517842c814ef74b2dcac9171c3b53bf466
tuned;

diff -r 2ea1bf517842 -r abc53a03ca1c src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Sat Jan 10 12:21:27 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Sat Jan 10 13:02:27 2015 +0100
@@ -12,8 +12,8 @@
   eqtype request
   val request: Time.time -> (unit -> unit) -> request
   val cancel: request -> bool
+  val future: Time.time -> unit future
   val shutdown: unit -> unit
-  val future: Time.time -> unit future
 end;
 
 structure Event_Timer: EVENT_TIMER =
@@ -99,31 +99,13 @@
       | NONE =>
           if is_shutdown_req st
           then SOME (false, shutdown_ack_state)
-          else NONE)) = SOME false
-  then () else manager_loop ();
+          else NONE)) <> SOME false
+  then manager_loop () else ();
 
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
   else SOME (Simple_Thread.fork false manager_loop);
 
-
-(* main operations *)
-
-fun request time event =
-  Synchronized.change_result state (fn State {requests, status, manager} =>
-    let
-      val req = new_request ();
-      val requests' = add_request time (req, event) requests;
-      val manager' = manager_check manager;
-    in (req, make_state (requests', status, manager')) end);
-
-fun cancel req =
-  Synchronized.change_result state (fn State {requests, status, manager} =>
-    let
-      val (canceled, requests') = del_request req requests;
-      val manager' = manager_check manager;
-    in (canceled, make_state (requests', status, manager')) end);
-
 fun shutdown () =
   uninterruptible (fn restore_attributes => fn () =>
     if Synchronized.change_result state (fn st as State {requests, status, manager} =>
@@ -143,7 +125,22 @@
     else ()) ();
 
 
-(* future *)
+(* main operations *)
+
+fun request time event =
+  Synchronized.change_result state (fn State {requests, status, manager} =>
+    let
+      val req = new_request ();
+      val requests' = add_request time (req, event) requests;
+      val manager' = manager_check manager;
+    in (req, make_state (requests', status, manager')) end);
+
+fun cancel req =
+  Synchronized.change_result state (fn State {requests, status, manager} =>
+    let
+      val (canceled, requests') = del_request req requests;
+      val manager' = manager_check manager;
+    in (canceled, make_state (requests', status, manager')) end);
 
 val future = uninterruptible (fn _ => fn time =>
   let