[isabelle-dev] NEWS

[Makarius]

* Parallel and asynchronous execution requires special care concerning
interrupts.  Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt.  User code must not absorb
interrupts -- intermediate handling (for cleanup etc.) needs to be
followed by re-raising of the original exception.  Another common
source of mistakes are "handle _" patterns, which make the meaning of
the program subject to physical effects of the environment.

(Strictly speaking the only new thing is the extension of structure Exn.)


 	Makarius