equal
deleted
inserted
replaced
128 then manager_loop () else (); |
128 then manager_loop () else (); |
129 |
129 |
130 fun manager_check manager = |
130 fun manager_check manager = |
131 if is_some manager andalso Thread.isActive (the manager) then manager |
131 if is_some manager andalso Thread.isActive (the manager) then manager |
132 else |
132 else |
133 SOME (Standard_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 restore_attributes => 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, ...} => |