1.1 --- a/src/Pure/Concurrent/future.ML	Fri Dec 07 20:39:09 2012 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Dec 07 23:11:01 2012 +0100
     1.3 @@ -385,7 +385,7 @@
     1.4  
     1.5      val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else ();
     1.6      val continue = not (! do_shutdown andalso null (! workers));
     1.7 -    val _ = if continue then () else scheduler := NONE;
     1.8 +    val _ = if continue then () else (report_status (); scheduler := NONE);
     1.9  
    1.10      val _ = broadcast scheduler_event;
    1.11    in continue end
    1.12 @@ -401,7 +401,7 @@
    1.13      Multithreading.with_attributes
    1.14        (Multithreading.sync_interrupts Multithreading.public_interrupts)
    1.15        (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
    1.16 -  do (); last_round := Time.zeroTime; report_status ());
    1.17 +  do (); last_round := Time.zeroTime);
    1.18  
    1.19  fun scheduler_active () = (*requires SYNCHRONIZED*)
    1.20    (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);