diff -r 4319691be975 -r 3dec88149176 NEWS
--- 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