src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Sat Feb 16 16:44:02 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Feb 16 16:44:02 2008 +0100
@@ -141,23 +141,25 @@
 local
 
 val sig_int = 2;
+val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
+
+val _ = Signal.signal (sig_int, default_handler);
 
 fun change_signal new_handler f x =
   let
-    (*RACE wrt. other signals*)
+    (*RACE wrt. other signals!*)
     val old_handler = Signal.signal (sig_int, new_handler);
-    val result = Exn.capture f x;
+    val result = Exn.capture (f old_handler) x;
     val _ = Signal.signal (sig_int, old_handler);
   in Exn.release result end;
 
-val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
-
 in
 
-val _ = Signal.signal (sig_int, default_handler);
+fun interruptible f = change_signal default_handler (fn _ => f);
 
-fun ignore_interrupt f = change_signal Signal.SIG_IGN f;
-fun raise_interrupt f = change_signal default_handler f;
+fun uninterruptible f =
+  change_signal Signal.SIG_IGN
+    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
 
 end;