tuned messages;
authorwenzelm
Tue, 26 Feb 2013 12:46:47 +0100
changeset 52416f4a2fa9286e9
parent 52415 1ee77b36490e
child 52417 12b7b0baaa1e
tuned messages;
src/Pure/Concurrent/future.ML
     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