NEWS
changeset 18686 cbbc71acf994
parent 18674 98d380757893
child 18687 af605e186480
     1.1 --- a/NEWS	Sat Jan 14 17:14:18 2006 +0100
     1.2 +++ b/NEWS	Sat Jan 14 17:15:24 2006 +0100
     1.3 @@ -333,6 +333,24 @@
     1.4  obsolete, it is ill-behaved in a local proof context (e.g. with local
     1.5  fixes/assumes or in a locale context).
     1.6  
     1.7 +* ML/Isar: simplified treatment of user-level errors, using exception
     1.8 +ERROR of string uniformly.  Function now error merely raises ERROR,
     1.9 +without any side effect on output channels.  The Isar toplevel takes
    1.10 +care of proper display of ERROR exceptions.  ML code may use plain
    1.11 +handle/can/try; cat_error may be used to concatenate errors like this:
    1.12 +
    1.13 +  ... handle ERROR msg => cat_error msg "..."
    1.14 +
    1.15 +Toplevel ML code (run directly or through the Isar toplevel) may be
    1.16 +embedded into the Isar exception display/debug facilities as follows:
    1.17 +
    1.18 +  Isar.toplevel (fn () => ...)
    1.19 +
    1.20 +INCOMPATIBILITY, removed special transform_error facilities, removed
    1.21 +obsolete variants of user-level exceptions (ERROR_MESSAGE,
    1.22 +Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
    1.23 +-- use plain ERROR instead.
    1.24 +
    1.25  * Pure/Isar: Toplevel.theory_to_proof admits transactions that modify
    1.26  the theory before entering a proof state.  Transactions now always see
    1.27  a quasi-functional intermediate checkpoint, both in interactive and