author | wenzelm |
Mon, 09 Nov 1998 11:08:42 +0100 | |
changeset 5812 | cbc106ddcc83 |
parent 5811 | 0867068942e6 |
child 5813 | 4eea84a9427d |
--- a/src/Pure/ML-Systems/mlworks.ML Mon Nov 09 11:00:44 1998 +0100 +++ b/src/Pure/ML-Systems/mlworks.ML Mon Nov 09 11:08:42 1998 +0100 @@ -91,6 +91,18 @@ +(** interrupts **) (*Note: may get into race conditions*) + +exception Interrupt; + +MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt); + +fun mask_interrupt f x = f x; +fun unmask_interrupt f x = f x; +fun exhibit_interrupt f x = f x; + + + (** OS related **) (* system command execution *)