equal
deleted
inserted
replaced
201 if tool' = tool then SOME (th, (tool', Time.now (), desc)) |
201 if tool' = tool then SOME (th, (tool', Time.now (), desc)) |
202 else NONE) active |
202 else NONE) active |
203 val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; |
203 val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; |
204 val _ = |
204 val _ = |
205 if null killing then () |
205 if null killing then () |
206 else Output.urgent_message ("Killed active " ^ das_wort_worker ^ "s.") |
206 else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.") |
207 in state' end); |
207 in state' end); |
208 |
208 |
209 |
209 |
210 (* running threads *) |
210 (* running threads *) |
211 |
211 |