# HG changeset patch
# User wenzelm
# Date 1237931777 -3600
# Node ID b1a87e3971a3a09b47078e2ea27999a4d3255a60
# Parent  fc9d8b1bf1e0ead8b1e4bbc4590652d58c225167
status_of: need to include local promises as well!

diff -r fc9d8b1bf1e0 -r b1a87e3971a3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Mar 24 22:55:49 2009 +0100
+++ b/src/Pure/thm.ML	Tue Mar 24 22:56:17 2009 +0100
@@ -60,7 +60,6 @@
   val theory_of_thm: thm -> theory
   val prop_of: thm -> term
   val tpairs_of: thm -> (term * term) list
-  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val concl_of: thm -> term
   val prems_of: thm -> term list
   val nprems_of: thm -> int
@@ -145,6 +144,7 @@
   val freezeT: thm -> thm
   val future: thm future -> cterm -> thm
   val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
+  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val join_proof: thm -> unit
@@ -400,7 +400,6 @@
 val hyps_of = #hyps o rep_thm;
 val prop_of = #prop o rep_thm;
 val tpairs_of = #tpairs o rep_thm;
-fun status_of (Thm (Deriv {body, ...}, _)) = Pt.status_of body;
 
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
@@ -1637,16 +1636,29 @@
   end;
 
 
-(* pending task groups *)
+(* derivation status *)
+
+fun raw_proof_body_of (Thm (Deriv {body, ...}, _)) = body;
+val raw_proof_of = Proofterm.proof_of o raw_proof_body_of;
 
 fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
   fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
 
+fun status_of (Thm (Deriv {promises, body, ...}, _)) =
+  let
+    val ps = map (Future.peek o snd) promises;
+    val bodies = body ::
+      map_filter (fn SOME (Exn.Result th) => SOME (raw_proof_body_of th) | _ => NONE) ps;
+    val {oracle, unfinished, failed} = Pt.status_of bodies;
+  in
+   {oracle = oracle,
+    unfinished = unfinished orelse exists is_none ps,
+    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
+  end;
+
 
 (* fulfilled proofs *)
 
-fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
-
 fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
   let
     val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));