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