[isabelle-dev] ML: distinguish proper interrupts from Poly/ML RTS breakdown

[Makarius]

*** 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.


Here is an artificial example:

ML ‹fun bad () = (Isabelle_Thread.expose_interrupt (); 1 + bad ())›

ML_val ‹Timeout.apply_physical (seconds 0.1) bad ()›  (*Timeout after 0.100s*)
ML_val ‹Timeout.apply_physical (seconds 0.5) bad ()›  (*Timeout after 1.866s*)
ML_val ‹Timeout.apply_physical (seconds 1.0) bad ()›  (*Timeout after 2.118s*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()›  (*exception 
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()›  (*Timeout after 4.546s*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()›  (*exception 
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)
ML_val ‹Timeout.apply_physical (seconds 2.5) bad ()›  (*exception 
Interrupt_Breakdown raised (line 77 of "./basis/PolyMLException.sml")*)


This shows that the result is a bit non-deterministic. It remains to be seen 
how usable it is in realistic applications.


	Makarius