132 else |
132 else |
133 SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} |
133 SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} |
134 manager_loop); |
134 manager_loop); |
135 |
135 |
136 fun shutdown () = |
136 fun shutdown () = |
137 Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
137 Thread_Attributes.uninterruptible (fn run => fn () => |
138 if Synchronized.change_result state (fn st as State {requests, manager, ...} => |
138 if Synchronized.change_result state (fn st as State {requests, manager, ...} => |
139 if is_shutdown Normal st then (false, st) |
139 if is_shutdown Normal st then (false, st) |
140 else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then |
140 else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then |
141 raise Fail "Concurrent attempt to shutdown event timer" |
141 raise Fail "Concurrent attempt to shutdown event timer" |
142 else (true, make_state (requests, Shutdown_Req, manager_check manager))) |
142 else (true, make_state (requests, Shutdown_Req, manager_check manager))) |
143 then |
143 then |
144 restore_attributes (fn () => |
144 run (fn () => |
145 Synchronized.guarded_access state |
145 Synchronized.guarded_access state |
146 (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) () |
146 (fn st => if is_shutdown Shutdown_Ack st then SOME ((), normal_state) else NONE)) () |
147 handle exn => |
147 handle exn => |
148 if Exn.is_interrupt exn then |
148 if Exn.is_interrupt exn then |
149 Synchronized.change state (fn State {requests, manager, ...} => |
149 Synchronized.change state (fn State {requests, manager, ...} => |