tuned messages;

--- 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 ();