# HG changeset patch
# User wenzelm
# Date 1354918261 -3600
# Node ID f8cd5e53653b98df3433356a94bbb3810042c626
# Parent  7a78a74139f54fca594217c24ec7a5da4a1a4a69
final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;

diff -r 7a78a74139f5 -r f8cd5e53653b src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Dec 07 20:39:09 2012 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Dec 07 23:11:01 2012 +0100
@@ -385,7 +385,7 @@
 
     val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else ();
     val continue = not (! do_shutdown andalso null (! workers));
-    val _ = if continue then () else scheduler := NONE;
+    val _ = if continue then () else (report_status (); scheduler := NONE);
 
     val _ = broadcast scheduler_event;
   in continue end
@@ -401,7 +401,7 @@
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do (); last_round := Time.zeroTime; report_status ());
+  do (); last_round := Time.zeroTime);
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);