ML: distinguish proper interrupts from Poly/ML RTS breakdown
ML
- Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.
This refers to Isabelle/280a228dc2f1.
- Projects
- Subscribers
- None