# 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 () =>