# HG changeset patch
# User wenzelm
# Date 1566057595 -7200
# Node ID 095dadc62bb536f3cbe7f34cfb85361531cdce28
# Parent  6e055d313f7356ee611501096ef1bf6776fcfd90
discontinued peek_status: unused and not clearly defined;

diff -r 6e055d313f73 -r 095dadc62bb5 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat Aug 17 17:59:55 2019 +0200
@@ -579,7 +579,6 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type thm} \\
-  @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   @{index_ML Thm.assume: "cterm -> thm"} \\
   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
@@ -602,13 +601,6 @@
   @{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\
   \end{mldecls}
 
-  \<^descr> \<^ML>\<open>Thm.peek_status\<close>~\<open>thm\<close> informs about the current status of the
-  derivation object behind the given theorem. This is a snapshot of a
-  potentially ongoing (parallel) evaluation of proofs. The three Boolean
-  values indicate the following: \<^verbatim>\<open>oracle\<close> if the finished part contains some
-  oracle invocation; \<^verbatim>\<open>unfinished\<close> if some future proofs are still pending;
-  \<^verbatim>\<open>failed\<close> if some future proof has failed, rendering the theorem invalid!
-
   \<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
   occurrences of the atomic term \<open>a\<close> in the body proposition \<open>B\<close> are replaced
   by bound variables. (See also \<^ML>\<open>lambda\<close> on terms.)
diff -r 6e055d313f73 -r 095dadc62bb5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 17 17:59:55 2019 +0200
@@ -56,7 +56,6 @@
     ({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
   val consolidate: proof_body list -> unit
-  val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
@@ -290,29 +289,6 @@
           in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
-fun peek_status bodies =
-  let
-    fun status (PBody {oracles, thms, ...}) x =
-      let
-        val ((oracle, unfinished, failed), seen) =
-          (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
-            if Inttab.defined seen i then (st, seen)
-            else
-              let val seen' = Inttab.update (i, ()) seen in
-                (case Future.peek (thm_node_body thm_node) of
-                  SOME (Exn.Res 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 (fold status bodies ((false, false, false), Inttab.empty));
-  in {oracle = oracle, unfinished = unfinished, failed = failed} end;
-
 
 (* proof body *)
 
diff -r 6e055d313f73 -r 095dadc62bb5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 17 17:59:55 2019 +0200
@@ -102,7 +102,6 @@
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val consolidate: thm list -> unit
-  val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
@@ -755,21 +754,6 @@
 val consolidate = ignore o proof_bodies_of;
 
 
-(* derivation status *)
-
-fun peek_status (Thm (Deriv {promises, body}, _)) =
-  let
-    val ps = map (Future.peek o snd) promises;
-    val bodies = body ::
-      map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
-    val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
-  in
-   {oracle = oracle,
-    unfinished = unfinished orelse exists is_none ps,
-    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
-  end;
-
-
 (* future rule *)
 
 fun future_result i orig_cert orig_shyps orig_prop thm =