# HG changeset patch
# User wenzelm
# Date 1361879207 -3600
# Node ID f4a2fa9286e970b2f411e5782761ccdb009dcc0f
# Parent  1ee77b36490e809df94ef41ea4993e796a9d37e2
tuned messages;

diff -r 1ee77b36490e -r f4a2fa9286e9 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Feb 26 11:57:19 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 26 12:46:47 2013 +0100
@@ -331,7 +331,7 @@
           val _ = workers := alive;
         in
           Multithreading.tracing 0 (fn () =>
-            "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
+            "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
         end;
 
 
@@ -398,7 +398,7 @@
   in continue end
   handle exn =>
     if Exn.is_interrupt exn then
-     (Multithreading.tracing 1 (fn () => "Interrupt");
+     (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
       List.app cancel_later (cancel_all ());
       broadcast_work (); true)
     else reraise exn;
@@ -684,8 +684,10 @@
 fun shutdown () =
   if Multithreading.available then
     SYNCHRONIZED "shutdown" (fn () =>
-     while scheduler_active () do
-      (wait scheduler_event; broadcast_work ()))
+      while scheduler_active () do
+       (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
+        wait scheduler_event;
+        broadcast_work ()))
   else ();