1.1 --- a/src/Pure/Concurrent/future.ML Tue Feb 26 11:57:19 2013 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Tue Feb 26 12:46:47 2013 +0100
1.3 @@ -331,7 +331,7 @@
1.4 val _ = workers := alive;
1.5 in
1.6 Multithreading.tracing 0 (fn () =>
1.7 - "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
1.8 + "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
1.9 end;
1.10
1.11
1.12 @@ -398,7 +398,7 @@
1.13 in continue end
1.14 handle exn =>
1.15 if Exn.is_interrupt exn then
1.16 - (Multithreading.tracing 1 (fn () => "Interrupt");
1.17 + (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
1.18 List.app cancel_later (cancel_all ());
1.19 broadcast_work (); true)
1.20 else reraise exn;
1.21 @@ -684,8 +684,10 @@
1.22 fun shutdown () =
1.23 if Multithreading.available then
1.24 SYNCHRONIZED "shutdown" (fn () =>
1.25 - while scheduler_active () do
1.26 - (wait scheduler_event; broadcast_work ()))
1.27 + while scheduler_active () do
1.28 + (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
1.29 + wait scheduler_event;
1.30 + broadcast_work ()))
1.31 else ();
1.32
1.33