# HG changeset patch # User wenzelm # Date 1247950289 -7200 # Node ID 8c391a12df1d62da01ca9cdce71c36e5d4329059 # Parent 82a9875b8707485ca17f1b3ecc3dd7435198cada added group_id; added status; diff -r 82a9875b8707 -r 8c391a12df1d src/Pure/Concurrent/task_queue.ML --- 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}) =