src/Pure/Concurrent/task_queue.ML

   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> task list -> (unit -> 'a) -> 'a
   type queue
   val empty: queue
+  val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int}
   val cancel: queue -> group -> bool
   val cancel_all: queue -> group list
   val finish: task -> queue -> bool * queue
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
-  val enqueue: string -> group -> task list -> int -> (bool -> bool) ->
-    queue -> (task * bool) * queue
+  val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool * queue
   val dequeue: Thread.thread -> queue -> (task * (bool -> bool) list) option * queue
   val dequeue_deps: Thread.thread -> task list -> queue ->
     (((task * (bool -> bool) list) option * task list) * queue)

   jobs: jobs};                      (*job dependency graph*)
 
 fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
 
 val empty = make_queue Inttab.empty Task_Graph.empty;
+
+fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
 
 (* job status *)
 
 fun ready_job task (Job list, ([], _)) = SOME (task, rev list)

     val groups' = groups
       |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
     val jobs' = jobs
       |> Task_Graph.new_node (task, Job [job])
       |> fold (add_job task) deps;
-    val minimal = null (get_deps jobs' task);
-  in ((task, minimal), make_queue groups' jobs') end;
+  in (task, make_queue groups' jobs') end;
 
 fun extend task job (Queue {groups, jobs}) =
   (case try (get_job jobs) task of
     SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
   | _ => NONE);