equal
deleted
inserted
replaced
103 then manager_loop () else (); |
103 then manager_loop () else (); |
104 |
104 |
105 fun manager_check manager = |
105 fun manager_check manager = |
106 if is_some manager andalso Thread.isActive (the manager) then manager |
106 if is_some manager andalso Thread.isActive (the manager) then manager |
107 else |
107 else |
108 SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} |
108 SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} |
109 manager_loop); |
109 manager_loop); |
110 |
110 |
111 fun shutdown () = |
111 fun shutdown () = |
112 uninterruptible (fn restore_attributes => fn () => |
112 uninterruptible (fn restore_attributes => fn () => |
113 if Synchronized.change_result state (fn st as State {requests, status, manager} => |
113 if Synchronized.change_result state (fn st as State {requests, status, manager} => |