# HG changeset patch
# User wenzelm
# Date 1296663967 -3600
# Node ID b828d4b533869085de80c5a2cd948063cdc8fe5a
# Parent  73dde8006820f39d84a5715466c4b1747717121b
refined Task_Queue.dequeue_deps (more incremental);

diff -r 73dde8006820 -r b828d4b53386 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Feb 02 15:04:09 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Feb 02 17:26:07 2011 +0100
@@ -262,8 +262,7 @@
       |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
     val jobs' = jobs
       |> Task_Graph.new_node (task, Job [job])
-      |> fold (add_job task) deps
-      |> fold (fold (add_job task) o get_deps jobs) deps;
+      |> fold (add_job task) deps;
     val minimal = null (get_deps jobs' task);
   in ((task, minimal), make_queue groups' jobs') end;
 
@@ -302,18 +301,35 @@
 
 fun dequeue_deps thread (Deps deps) (queue as Queue {groups, jobs}) =
   let
-    fun ready task = ready_job task (Task_Graph.get_entry jobs task);
-    val tasks = filter (can (Task_Graph.get_node jobs)) deps;
-    fun result (res as (task, _)) =
+    fun ready [] rest = (NONE, rev rest)
+      | ready (task :: tasks) rest =
+          (case try (Task_Graph.get_entry jobs) task of
+            NONE => ready tasks rest
+          | SOME entry =>
+              (case ready_job task entry of
+                NONE => ready tasks (task :: rest)
+              | some => (some, List.revAppend (rest, tasks))));
+
+    fun ready_dep _ [] = NONE
+      | ready_dep seen (task :: tasks) =
+          if member eq_task seen task then ready_dep seen tasks
+          else
+            let val entry as (_, (ds, _)) = Task_Graph.get_entry jobs task in
+              (case ready_job task entry of
+                NONE => ready_dep (task :: seen) (ds @ tasks)
+              | some => some)
+            end;
+
+    fun result (res as (task, _)) deps' =
       let val jobs' = set_job task (Running thread) jobs
-      in ((SOME res, Deps tasks), make_queue groups jobs') end;
+      in ((SOME res, Deps deps'), make_queue groups jobs') end;
   in
-    (case get_first ready tasks of
-      SOME res => result res
-    | NONE =>
-        (case get_first (get_first ready o get_deps jobs) tasks of
-          SOME res => result res
-        | NONE => ((NONE, Deps tasks), queue)))
+    (case ready deps [] of
+      (SOME res, deps') => result res deps'
+    | (NONE, deps') =>
+        (case ready_dep [] deps' of
+          SOME res => result res deps'
+        | NONE => ((NONE, Deps deps'), queue)))
   end;
 
 end;