# HG changeset patch
# User wenzelm
# Date 1248526725 -7200
# Node ID eb09607094b3c8c8761302306616bffdf326aaf5
# Parent  348a66f821bf4dc41b3186e1157c35a260e8515f
dequeue_towards: need to try imm_preds as well;

diff -r 348a66f821bf -r eb09607094b3 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Jul 25 14:32:35 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Jul 25 14:58:45 2009 +0200
@@ -210,14 +210,18 @@
           else NONE
       | _ => NONE);
     val tasks = filter (can (Task_Graph.get_node jobs)) deps;
+    fun result (res as (task, _, _)) =
+      let
+        val jobs' = set_job task (Running (Thread.self ())) jobs;
+        val cache' = Unknown;
+      in (SOME (res, tasks), make_queue groups jobs' cache') end;
   in
     (case get_first ready tasks of
-      SOME (res as (task, _, _)) =>
-        let
-          val jobs' = set_job task (Running (Thread.self ())) jobs;
-          val cache' = Unknown;
-        in (SOME (res, tasks), make_queue groups jobs' cache') end
-    | NONE => (NONE, queue))
+      SOME res => result res
+    | NONE =>
+        (case get_first (get_first ready o Task_Graph.imm_preds jobs) tasks of
+          SOME res => result res
+        | NONE => (NONE, queue)))
   end;