src/Pure/Concurrent/future.ML

         let
           val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
           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;
 
 
     (* worker pool adjustments *)
 

 
     val _ = broadcast scheduler_event;
   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;
 
 fun scheduler_loop () =

 (* shutdown *)
 
 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 ();
 
 
 (*final declarations of this structure!*)
 val map = map_future;