NEWS
changeset 18687 af605e186480
parent 18686 cbbc71acf994
child 18694 83f50ac6ddcb
     1.1 --- a/NEWS	Sat Jan 14 17:15:24 2006 +0100
     1.2 +++ b/NEWS	Sat Jan 14 17:20:51 2006 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4  fixes/assumes or in a locale context).
     1.5  
     1.6  * ML/Isar: simplified treatment of user-level errors, using exception
     1.7 -ERROR of string uniformly.  Function now error merely raises ERROR,
     1.8 +ERROR of string uniformly.  Function error now 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 @@ -342,7 +342,8 @@
    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 +embedded into the Isar toplevel with exception display/debug like
    1.18 +this:
    1.19  
    1.20    Isar.toplevel (fn () => ...)
    1.21