# HG changeset patch
# User wenzelm
# Date 1257331026 -3600
# Node ID 0a1c0c1209ec97aa52939b07e8ada495f82d8d7c
# Parent  a69ddd7dce953445daf8f39f125957632800c25c
tuned;

diff -r a69ddd7dce95 -r 0a1c0c1209ec src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Nov 04 11:30:22 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Nov 04 11:37:06 2009 +0100
@@ -205,14 +205,14 @@
     val _ = active := true;
   in () end;
 
-fun worker_next has_work = (*requires SYNCHRONIZED*)
+fun worker_next have_work = (*requires SYNCHRONIZED*)
   if length (! workers) > ! max_workers then
     (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
+     if have_work then signal work_available else ();
      broadcast scheduler_event;
-     if has_work then signal work_available else ();
      NONE)
   else if count_active () > ! max_active then
-    (if has_work then signal work_available else ();
+    (if have_work then signal work_available else ();
      worker_wait scheduler_event;
      worker_next false)
   else
@@ -267,11 +267,13 @@
     val _ =
       if forall (Thread.isActive o #1) (! workers) then ()
       else
-        (case List.partition (Thread.isActive o #1) (! workers) of
-          (_, []) => ()
-        | (alive, dead) =>
-            (workers := alive; Multithreading.tracing 0 (fn () =>
-              "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")));
+        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")
+        end;
 
     val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
     val _ = max_active := m;
@@ -363,7 +365,7 @@
       Exn.Exn (Exn.EXCEPTIONS (Exn.flatten_list (Task_Queue.group_status (group_of x))))
   | SOME res => res);
 
-fun join_wait x =
+fun passive_wait x =
   Synchronized.readonly_access (result_of x) (fn NONE => NONE | SOME _ => SOME ());
 
 fun join_next deps = (*requires SYNCHRONIZED*)
@@ -392,7 +394,7 @@
   else
     (case worker_task () of
       SOME task => join_depend task (map task_of xs)
-    | NONE => List.app join_wait xs;
+    | NONE => List.app passive_wait xs;
     map get_result xs);
 
 end;