# HG changeset patch
# User wenzelm
# Date 1248164596 -7200
# Node ID 30996b775a7ff7bb08abc5d6ec7d3040411d221b
# Parent  6a599543826625c8f3a2e49386ac7bc25ddfaa9c
tuned dequeu_towards: try immediate tasks before expensive all_preds;

diff -r 6a5995438266 -r 30996b775a7f src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Jul 21 01:05:10 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Jul 21 10:23:16 2009 +0200
@@ -162,15 +162,20 @@
           if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
           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 (Task_Graph.all_preds jobs tasks) of
-      NONE => (NONE, queue)
-    | SOME (result as (task, _, _)) =>
-        let
-          val jobs' = set_job task (Running (Thread.self ())) jobs;
-          val cache' = Unknown;
-        in (SOME (result, tasks), make_queue groups jobs' cache') end)
+    (case get_first ready tasks of
+      SOME res => result res
+    | NONE =>
+        (case get_first ready (Task_Graph.all_preds jobs tasks) of
+          SOME res => result res
+        | NONE => (NONE, queue)))
   end;