theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;

--- a/NEWS	Mon Nov 19 18:01:48 2012 +0100
+++ b/NEWS	Mon Nov 19 20:23:47 2012 +0100
@@ -6,6 +6,14 @@
 
 *** General ***
 
+* Theorem status about oracles and unfinished/failed future proofs is
+no longer printed by default, since it is incompatible with
+incremental / parallel checking of the persistent document model.  ML
+function Thm.peek_status may be used to inspect a snapshot of the
+ongoing evaluation process.  Note that in batch mode --- notably
+isabelle build --- the system ensures that future proofs of all
+accessible theorems in the theory context are finished (as before).
+
 * Configuration option show_markup controls direct inlining of markup
 into the printed representation of formal entities --- notably type
 and sort constraints.  This enables Prover IDE users to retrieve that

--- a/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 20:23:47 2012 +0100
@@ -648,6 +648,7 @@
   \begin{mldecls}
   @{index_ML_type thm} \\
   @{index_ML proofs: "int Unsynchronized.ref"} \\
+  @{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"} \\
@@ -670,6 +671,15 @@
 
   \begin{description}
 
+  \item @{ML Thm.peek_status}~@{text "thm"} 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 oracle}
+  if the finished part contains some oracle invocation; @{verbatim
+  unfinished} if some future proofs are still pending; @{verbatim
+  failed} if some future proof has failed, rendering the theorem
+  invalid!
+
   \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
   @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
   the body proposition @{text "B"} are replaced by bound variables.

--- a/src/Doc/IsarRef/Proof.thy	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Mon Nov 19 20:23:47 2012 +0100
@@ -670,9 +670,9 @@
   pretending to solve the pending claim without further ado.  This
   only works in interactive development, or if the @{ML
   quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
-  proofs are not the real thing.  Internally, each theorem container
-  is tainted by an oracle invocation, which is indicated as ``@{text
-  "[!]"}'' in the printed result.
+  proofs are not the real thing.  Internally, the derivation object is
+  tainted by an oracle invocation, which may be inspected via the
+  theorem status \cite{isabelle-implementation}.
   
   The most important application of @{command "sorry"} is to support
   experimentation and top-down proof development.

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -963,7 +963,7 @@
           val (proved, unproved) = partition_vcs vcs;
           val _ = Thm.join_proofs (maps (#2 o snd) proved);
           val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
-            exists (#oracle o Thm.status_of) thms) proved
+            exists (#oracle o Thm.peek_status) thms) proved
         in
           (if null unproved then ()
            else (if incomplete then warning else error)

--- a/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 20:23:47 2012 +0100
@@ -34,7 +34,7 @@
 
 ML {* iff_oracle (@{theory}, 2) *}
 ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
+ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
 
 text {* These oracle calls had better fail. *}
 

--- a/src/Pure/Isar/proof_context.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -52,7 +52,6 @@
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val markup_fact: Proof.context -> string -> Markup.T
-  val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val read_class: Proof.context -> xstring -> class
   val read_typ: Proof.context -> string -> typ
@@ -343,14 +342,11 @@
 fun pretty_fact_name ctxt a =
   Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
 
-fun pretty_fact_aux ctxt flag ("", ths) =
-      Display.pretty_thms_aux ctxt flag ths
-  | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
-      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
-  | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
-      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
-
-fun pretty_fact ctxt = pretty_fact_aux ctxt true;
+fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths
+  | pretty_fact ctxt (a, [th]) = Pretty.block
+      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th]
+  | pretty_fact ctxt (a, ths) = Pretty.block
+      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths));
 
 
 

--- a/src/Pure/Isar/proof_display.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Pure/Isar/proof_display.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -46,10 +46,8 @@
   | NONE => Syntax.init_pretty_global thy0);
 
 fun pp_thm th =
-  let
-    val ctxt = default_context (Thm.theory_of_thm th);
-    val flags = {quote = true, show_hyps = false, show_status = true};
-  in Display.pretty_thm_raw ctxt flags th end;
+  let val ctxt = default_context (Thm.theory_of_thm th);
+  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
 
 fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
 fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
@@ -85,7 +83,7 @@
 
 fun pretty_rule ctxt s thm =
   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
-    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
+    Pretty.fbrk, Display.pretty_thm ctxt thm];
 
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
@@ -138,7 +136,7 @@
 
 fun pretty_facts ctxt =
   flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
-    map (single o Proof_Context.pretty_fact_aux ctxt false);
+    map (single o Proof_Context.pretty_fact ctxt);
 
 in
 
@@ -151,7 +149,7 @@
     (Pretty.writeln o Pretty.mark markup)
       (case facts of
         [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
-          Proof_Context.pretty_fact_aux ctxt false fact])
+          Proof_Context.pretty_fact ctxt fact])
       | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 

--- a/src/Pure/display.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Pure/display.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -18,16 +18,13 @@
 signature DISPLAY =
 sig
   include BASIC_DISPLAY
-  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
-    thm -> Pretty.T
-  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
+  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thm_global: theory -> thm -> Pretty.T
   val pretty_thm_without_context: thm -> Pretty.T
   val string_of_thm: Proof.context -> thm -> string
   val string_of_thm_global: theory -> thm -> string
   val string_of_thm_without_context: thm -> string
-  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
   val pretty_thms: Proof.context -> thm list -> Pretty.T
   val print_syntax: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T list
@@ -54,20 +51,7 @@
 fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
-fun display_status _ false _ = ""
-  | display_status show_hyps true 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_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
+fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
   let
     val show_tags = Config.get ctxt show_tags;
     val show_hyps = Config.get ctxt show_hyps;
@@ -82,30 +66,24 @@
 
     val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
     val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
-    val status = display_status show_hyps show_status th;
 
     val hlen = length xshyps + length hyps' + length tpairs;
     val hsymbs =
-      if hlen = 0 andalso status = "" then []
+      if hlen = 0 then []
       else if show_hyps orelse show_hyps' then
         [Pretty.brk 2, Pretty.list "[" "]"
           (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
-           map (Syntax.pretty_sort ctxt) xshyps @
-            (if status = "" then [] else [Pretty.str status]))]
-      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
+           map (Syntax.pretty_sort ctxt) xshyps)]
+      else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
     val tsymbs =
       if null tags orelse not show_tags then []
       else [Pretty.brk 1, pretty_tags tags];
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
-fun pretty_thm_aux ctxt show_status =
-  pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
-
-fun pretty_thm ctxt = pretty_thm_aux ctxt true;
+fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
 
 fun pretty_thm_global thy =
-  pretty_thm_raw (Syntax.init_pretty_global thy)
-    {quote = false, show_hyps = false, show_status = true};
+  pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
 
 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
 
@@ -116,11 +94,8 @@
 
 (* multiple theorems *)
 
-fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
-  | pretty_thms_aux ctxt flag ths =
-      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
-
-fun pretty_thms ctxt = pretty_thms_aux ctxt true;
+fun pretty_thms ctxt [th] = pretty_thm ctxt th
+  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
 
 
 

--- a/src/Pure/proofterm.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Pure/proofterm.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -42,7 +42,7 @@
   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 join_bodies: proof_body list -> unit
-  val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
+  val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
@@ -208,7 +208,7 @@
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
 
-fun status_of bodies =
+fun peek_status bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
       let

--- a/src/Pure/thm.ML	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Pure/thm.ML	Mon Nov 19 20:23:47 2012 +0100
@@ -99,7 +99,7 @@
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val join_proofs: thm list -> unit
-  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
+  val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_name: thm -> string
   val name_derivation: string -> thm -> thm
@@ -536,12 +536,12 @@
 
 (* derivation status *)
 
-fun status_of (Thm (Deriv {promises, body}, _)) =
+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.status_of bodies;
+    val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
   in
    {oracle = oracle,
     unfinished = unfinished orelse exists is_none ps,