# HG changeset patch
# User wenzelm
# Date 1231602895 -3600
# Node ID 5bb5551bef03094154729b22645ff0ec8b606658
# Parent  0ebe652bfd5ab212b011799f4fa7d09dc33335d1
added pending_groups -- accumulates task groups of local derivations only;

diff -r 0ebe652bfd5a -r 5bb5551bef03 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jan 10 16:53:12 2009 +0100
+++ b/src/Pure/thm.ML	Sat Jan 10 16:54:55 2009 +0100
@@ -146,6 +146,7 @@
   val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val freezeT: thm -> thm
   val future: thm future -> cterm -> thm
+  val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val join_proof: thm -> unit
@@ -1626,7 +1627,13 @@
   end;
 
 
-(* fulfilled proof *)
+(* pending task groups *)
+
+fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
+  fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
+
+
+(* fulfilled proofs *)
 
 fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;