--- a/src/Pure/Concurrent/task_queue.ML Sat Jul 18 22:45:33 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Sat Jul 18 22:51:29 2009 +0200
@@ -11,6 +11,7 @@
val pri_of_task: task -> int
val str_of_task: task -> string
type group
+ val group_id: group -> int
val eq_group: group * group -> bool
val new_group: unit -> group
val is_valid: group -> bool
@@ -19,6 +20,7 @@
type queue
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 extend: task -> (bool -> bool) -> queue -> queue option
val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
@@ -47,6 +49,8 @@
(* groups *)
datatype group = Group of serial * bool ref;
+
+fun group_id (Group (gid, _)) = gid;
fun eq_group (Group (gid1, _), Group (gid2, _)) = gid1 = gid2;
fun new_group () = Group (serial (), ref true);
@@ -89,6 +93,19 @@
fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs;
+(* status *)
+
+fun status (Queue {jobs, ...}) =
+ let
+ val (x, y, z) =
+ Task_Graph.fold (fn (task, ((_, job), (deps, _))) => fn (x, y, z) =>
+ (case job of
+ Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z)
+ | Running _ => (x, y, z + 1)))
+ jobs (0, 0, 0);
+ in {ready = x, pending = y, running = z} end;
+
+
(* enqueue *)
fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =