* 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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
