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