# HG changeset patch
# User wenzelm
# Date 910606122 -3600
# Node ID cbc106ddcc83eba04d45a06a809793fd44c3bf13
# Parent  0867068942e660fc7386e38a938a9f384f87bb89
simple interrupt_handler;

diff -r 0867068942e6 -r cbc106ddcc83 src/Pure/ML-Systems/mlworks.ML
--- 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 *)