tuned dequeu_towards: try immediate tasks before expensive all_preds;

--- 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;