tuned;

--- a/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:35:27 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Jul 28 14:43:46 2009 +0200
@@ -94,6 +94,12 @@
 fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
 fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs;
 
+fun add_job task dep (jobs: jobs) =
+  Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
+
+fun get_deps (jobs: jobs) task =
+  Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
+
 
 (* queue of grouped jobs *)
 
@@ -147,12 +153,6 @@
 
 (* enqueue *)
 
-fun add_job task dep (jobs: jobs) =
-  Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
-
-fun get_deps (jobs: jobs) task =
-  Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
-
 fun enqueue group deps pri job (Queue {groups, jobs, cache}) =
   let
     val task = new_task pri;
@@ -206,7 +206,7 @@
     fun ready task =
       (case Task_Graph.get_node jobs task of
         (group, Job list) =>
-          if null (Task_Graph.imm_preds jobs task)
+          if null (get_deps jobs task)
           then SOME (task, group, rev list)
           else NONE
       | _ => NONE);
@@ -220,7 +220,7 @@
     (case get_first ready tasks of
       SOME res => result res
     | NONE =>
-        (case get_first (get_first ready o Task_Graph.imm_preds jobs) tasks of
+        (case get_first (get_first ready o get_deps jobs) tasks of
           SOME res => result res
         | NONE => ((NONE, tasks), queue)))
   end;