added is_empty;

--- a/src/Pure/Concurrent/task_queue.ML	Thu Sep 11 21:04:05 2008 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Sep 11 21:04:07 2008 +0200
@@ -14,6 +14,7 @@
   val str_of_group: group -> string
   type queue
   val empty: queue
+  val is_empty: queue -> bool
   val enqueue: group -> task list -> (bool -> bool) -> queue -> task * queue
   val depend: task list -> task -> queue -> queue
   val focus: task list -> queue -> queue
@@ -67,7 +68,9 @@
   focus: task list};                (*particular collection of high-priority tasks*)
 
 fun make_queue groups jobs focus = Queue {groups = groups, jobs = jobs, focus = focus};
+
 val empty = make_queue Inttab.empty IntGraph.empty [];
+fun is_empty (Queue {jobs, ...}) = IntGraph.is_empty jobs;
 
 
 (* enqueue *)

--- a/src/Pure/General/graph.ML	Thu Sep 11 21:04:05 2008 +0200
+++ b/src/Pure/General/graph.ML	Thu Sep 11 21:04:07 2008 +0200
@@ -13,6 +13,7 @@
   exception SAME
   exception UNDEF of key
   val empty: 'a T
+  val is_empty: 'a T -> bool
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list
   val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
@@ -83,6 +84,7 @@
 exception SAME = Table.SAME;
 
 val empty = Graph Table.empty;
+fun is_empty (Graph tab) = Table.is_empty tab;
 fun keys (Graph tab) = Table.keys tab;
 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);