src/Pure/Concurrent/event_timer.ML

--- a/src/Pure/Concurrent/event_timer.ML	Fri Jan 09 11:51:02 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Fri Jan 09 19:20:00 2015 +0100
@@ -64,34 +64,38 @@
 
 (* global state *)
 
-type state = requests * Thread.thread option;
-val init_state: state = (Requests.empty, NONE);
+datatype status = Normal | Shutdown_Req | Shutdown_Ack;
+
+datatype state =
+  State of {requests: requests, status: status, manager: Thread.thread option};
+
+fun make_state (requests, status, manager) =
+  State {requests = requests, status = status, manager = manager};
 
-val state = Synchronized.var "Event_Timer.state" init_state;
+val normal_state = make_state (Requests.empty, Normal, NONE);
+val shutdown_ack_state = make_state (Requests.empty, Shutdown_Ack, NONE);
+
+fun is_shutdown s (State {requests, status, manager}) =
+  Requests.is_empty requests andalso status = s andalso is_none manager;
+
+fun is_shutdown_req (State {requests, status, ...}) =
+  Requests.is_empty requests andalso status = Shutdown_Req;
+
+val state = Synchronized.var "Event_Timer.state" normal_state;
 
 
 (* manager thread *)
 
-val manager_timeout = seconds 0.3;
-
 fun manager_loop () =
-  let
-    val success =
-      Synchronized.timed_access state
-        (fn (requests, _) =>
-          (case next_request_time requests of
-            NONE => SOME (Time.+ (Time.now (), manager_timeout))
-          | some => some))
-        (fn (requests, manager) =>
-          (case next_request_event (Time.now ()) requests of
-            NONE => NONE
-          | SOME (event, requests') => (Exn.capture event (); SOME ((), (requests', manager)))));
-    val finished =
-      is_none success andalso
-        Synchronized.change_result state (fn (requests, manager) =>
-          if Requests.is_empty requests then (true, init_state)
-          else (false, (requests, manager)));
-  in if finished then () else manager_loop () end;
+  if Synchronized.timed_access state
+    (fn State {requests, ...} => next_request_time requests)
+    (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)))
+      | NONE =>
+          if is_shutdown_req st then SOME (false, shutdown_ack_state) else NONE)) = SOME false
+  then () else manager_loop ();
 
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
@@ -101,24 +105,35 @@
 (* main operations *)
 
 fun request time event =
-  Synchronized.change_result state (fn (requests, manager) =>
+  Synchronized.change_result state (fn State {requests, status, manager} =>
     let
       val req = new_request ();
       val requests' = add_request time (req, event) requests;
-    in (req, (requests', manager_check manager)) end);
+    in (req, make_state (requests', status, manager_check manager)) end);
 
 fun cancel req =
-  Synchronized.change_result state (fn (requests, manager) =>
+  Synchronized.change_result state (fn State {requests, status, manager} =>
     let
       val (canceled, requests') = del_request req requests;
-    in (canceled, (requests', manager)) end);
+    in (canceled, make_state (requests', status, manager_check manager)) end);
 
 fun shutdown () =
-  Synchronized.guarded_access state (fn (requests, manager) =>
-    if not (Requests.is_empty requests)
-    then raise Fail "Cannot shutdown event timer: pending requests"
-    else if is_none manager then SOME ((), init_state)
-    else NONE);
+  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
+        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 () =>
+        Synchronized.guarded_access state
+          (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) ()
+      handle exn =>
+        if Exn.is_interrupt exn then
+          Synchronized.change state (fn State {requests, manager, ...} =>
+            make_state (requests, Normal, manager))
+        else ()
+    else ()) ();
 
 
 (* future *)