# HG changeset patch
# User wenzelm
# Date 1420886932 -3600
# Node ID 6adaa4a17cfbc4e1f8aae3bcf872641d1773f8a1
# Parent  e743ce816cf6108178ab27ed098d2078cccc56ba
tuned;

diff -r e743ce816cf6 -r 6adaa4a17cfb src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Sat Jan 10 10:40:11 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Sat Jan 10 11:48:52 2015 +0100
@@ -92,9 +92,14 @@
     (fn st as State {requests, status, manager} =>
       (case next_request_event (Time.now ()) requests of
         SOME (event, requests') =>
-          (Exn.capture event (); SOME (true, make_state (requests', status, manager)))
+          let
+            val _ = Exn.capture event ();
+            val state' = make_state (requests', status, manager);
+          in SOME (true, state') end
       | NONE =>
-          if is_shutdown_req st then SOME (false, shutdown_ack_state) else NONE)) = SOME false
+          if is_shutdown_req st
+          then SOME (false, shutdown_ack_state)
+          else NONE)) = SOME false
   then () else manager_loop ();
 
 fun manager_check manager =
@@ -109,20 +114,22 @@
     let
       val req = new_request ();
       val requests' = add_request time (req, event) requests;
-    in (req, make_state (requests', status, manager_check manager)) end);
+      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;
-    in (canceled, make_state (requests', status, manager_check manager)) end);
+      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} =>
-      if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
+      if is_shutdown Normal st then (false, st)
+      else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
         raise Fail "Concurrent attempt to shutdown event timer"
-      else if is_shutdown Normal st then (false, st)
       else (true, make_state (requests, Shutdown_Req, manager_check manager)))
     then
       restore_attributes (fn () =>