diff -r 2f3d65d15149 -r 222f26693757 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sun Jul 26 22:33:32 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jul 27 12:00:02 2009 +0200
@@ -20,7 +20,7 @@
   val empty: queue
   val is_empty: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int}
-  val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
+  val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
   val dequeue_towards: task list -> queue ->
@@ -31,7 +31,7 @@
   val cancel_group: group -> exn -> unit
   val cancel: queue -> group -> bool
   val cancel_all: queue -> group list
-  val finish: task -> queue -> queue
+  val finish: task -> queue -> bool * queue
 end;
 
 structure Task_Queue:> TASK_QUEUE =
@@ -162,13 +162,14 @@
       |> Task_Graph.new_node (task, (group, Job [job]))
       |> fold (add_job task) deps
       |> fold (fold (add_job task) o get_deps jobs) deps;
+    val minimal = null (get_deps jobs' task);
     val cache' =
       (case cache of
         Result last =>
           if task_ord (last, task) = LESS
           then cache else Unknown
       | _ => Unknown);
-  in (task, make_queue groups' jobs' cache') end;
+  in ((task, minimal), make_queue groups' jobs' cache') end;
 
 fun extend task job (Queue {groups, jobs, cache}) =
   (case try (get_job jobs) task of
@@ -249,9 +250,8 @@
     val groups' = groups
       |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group);
     val jobs' = Task_Graph.del_node task jobs;
-    val cache' =
-      if null (Task_Graph.imm_succs jobs task) then cache
-      else Unknown;
-  in make_queue groups' jobs' cache' end;
+    val maximal = null (Task_Graph.imm_succs jobs task);
+    val cache' = if maximal then cache else Unknown;
+  in (maximal, make_queue groups' jobs' cache') end;
 
 end;