# HG changeset patch
# User wenzelm
# Date 1137255324 -3600
# Node ID cbbc71acf9948e2ad02567f0cec5c5f5eddcbd7c
# Parent  725660906cb3cd1649dc1db67bdf97da341b545a
* ML/Isar: simplified treatment of user-level errors;

diff -r 725660906cb3 -r cbbc71acf994 NEWS
--- a/NEWS	Sat Jan 14 17:14:18 2006 +0100
+++ b/NEWS	Sat Jan 14 17:15:24 2006 +0100
@@ -333,6 +333,24 @@
 obsolete, it is ill-behaved in a local proof context (e.g. with local
 fixes/assumes or in a locale context).
 
+* ML/Isar: simplified treatment of user-level errors, using exception
+ERROR of string uniformly.  Function now error merely raises ERROR,
+without any side effect on output channels.  The Isar toplevel takes
+care of proper display of ERROR exceptions.  ML code may use plain
+handle/can/try; cat_error may be used to concatenate errors like this:
+
+  ... handle ERROR msg => cat_error msg "..."
+
+Toplevel ML code (run directly or through the Isar toplevel) may be
+embedded into the Isar exception display/debug facilities as follows:
+
+  Isar.toplevel (fn () => ...)
+
+INCOMPATIBILITY, removed special transform_error facilities, removed
+obsolete variants of user-level exceptions (ERROR_MESSAGE,
+Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
+-- use plain ERROR instead.
+
 * Pure/Isar: Toplevel.theory_to_proof admits transactions that modify
 the theory before entering a proof state.  Transactions now always see
 a quasi-functional intermediate checkpoint, both in interactive and