# HG changeset patch
# User wenzelm
# Date 1361880348 -3600
# Node ID c05f7e1dd6023d8396832d5c1893071049a88318
# Parent  12b7b0baaa1eb4842d7483bc8a669a6925b9c57b
signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;

diff -r 12b7b0baaa1e -r c05f7e1dd602 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Feb 26 12:50:52 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 26 13:05:48 2013 +0100
@@ -154,10 +154,6 @@
 fun broadcast cond = (*requires SYNCHRONIZED*)
   ConditionVar.broadcast cond;
 
-fun broadcast_work () = (*requires SYNCHRONIZED*)
- (ConditionVar.broadcast work_available;
-  ConditionVar.broadcast work_finished);
-
 end;
 
 
@@ -380,7 +376,7 @@
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
         Unsynchronized.change canceled (filter_out (null o cancel_now));
-        broadcast_work ());
+        signal work_available);
 
 
     (* delay loop *)
@@ -400,7 +396,7 @@
     if Exn.is_interrupt exn then
      (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
       List.app cancel_later (cancel_all ());
-      broadcast_work (); true)
+      signal work_available; true)
     else reraise exn;
 
 fun scheduler_loop () =