display derivation status of thms;

--- a/src/Pure/display.ML	Tue Mar 24 19:37:50 2009 +0100
+++ b/src/Pure/display.ML	Tue Mar 24 21:24:53 2009 +0100
@@ -57,6 +57,18 @@
 fun pretty_flexpair pp (t, u) = Pretty.block
   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
 
+fun display_status th =
+  let
+    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
+    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
+  in
+    if failed then "!!"
+    else if oracle andalso unfinished then "!?"
+    else if oracle then "!"
+    else if unfinished then "?"
+    else ""
+  end;
+
 fun pretty_thm_aux pp quote show_hyps' asms raw_th =
   let
     val th = Thm.strip_shyps raw_th;
@@ -68,20 +80,17 @@
     val prt_term = q o Pretty.term pp;
 
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
-(* FIXME
-    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
-    val ora' = false;
+    val status = display_status th;
 
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =
-      if hlen = 0 andalso not ora' then []
+      if hlen = 0 andalso status = "" then []
       else if ! show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
            map (Pretty.sort pp) xshyps @
-            (if ora' then [Pretty.str "!"] else []))]
-      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
-        (if ora' then "!" else "") ^ "]")];
+            (if status = "" then [] else [Pretty.str status]))]
+      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
     val tsymbs =
       if null tags orelse not (! show_tags) then []
       else [Pretty.brk 1, pretty_tags tags];

--- a/src/Pure/proofterm.ML	Tue Mar 24 19:37:50 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Mar 24 21:24:53 2009 +0100
@@ -40,8 +40,9 @@
     {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
   val join_proof: proof_body future -> proof
   val proof_of: proof_body -> proof
+  val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
-  val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
+  val status_of: proof_body -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
@@ -159,17 +160,6 @@
 
 (***** proof atoms *****)
 
-fun fold_body_thms f =
-  let
-    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
-      if Inttab.defined seen i then (x, seen)
-      else
-        let
-          val body' = Future.join body;
-          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-        in (f (name, prop, body') x', seen') end);
-  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
-
 fun fold_proof_atoms all f =
   let
     fun app (Abst (_, _, prf)) = app prf
@@ -185,6 +175,39 @@
       | app prf = (fn (x, seen) => (f prf x, seen));
   in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
 
+fun fold_body_thms f =
+  let
+    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+      if Inttab.defined seen i then (x, seen)
+      else
+        let
+          val body' = Future.join body;
+          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+        in (f (name, prop, body') x', seen') end);
+  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
+
+fun status_of proof_body =
+  let
+    fun status (PBody {oracles, thms, ...}) x =
+      let
+        val ((oracle, unfinished, failed), seen) =
+          (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) =>
+            if Inttab.defined seen i then (st, seen)
+            else
+              let val seen' = Inttab.update (i, ()) seen in
+                (case Future.peek body of
+                  SOME (Exn.Result body') => status body' (st, seen')
+                | SOME (Exn.Exn _) =>
+                    let val (oracle, unfinished, _) = st
+                    in ((oracle, unfinished, true), seen') end
+                | NONE =>
+                    let val (oracle, _, failed) = st
+                    in ((oracle, true, failed), seen') end)
+              end);
+      in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
+    val (oracle, unfinished, failed) = #1 (status proof_body ((false, false, false), Inttab.empty));
+  in {oracle = oracle, unfinished = unfinished, failed = failed} end;
+
 
 (* proof body *)
 

--- a/src/Pure/thm.ML	Tue Mar 24 19:37:50 2009 +0100
+++ b/src/Pure/thm.ML	Tue Mar 24 21:24:53 2009 +0100
@@ -60,6 +60,7 @@
   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
@@ -399,6 +400,7 @@
 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;