# HG changeset patch
# User wenzelm
# Date 1203176642 -3600
# Node ID a7475459c7402b9bddbdf4d9d4b7cd045eda8ef9
# Parent  abb3f8dd66dcb7bc0fcfc1b03b87fd56c56b2352
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

diff -r abb3f8dd66dc -r a7475459c740 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Sat Feb 16 16:44:02 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML	Sat Feb 16 16:44:02 2008 +0100
@@ -126,8 +126,8 @@
 
 exception Interrupt;
 
-fun ignore_interrupt f x = f x;
-fun raise_interrupt f x = f x;
+fun interruptible f x = f x;
+fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
 
 
 (* basis library fixes *)
diff -r abb3f8dd66dc -r a7475459c740 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Feb 16 16:44:02 2008 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Sat Feb 16 16:44:02 2008 +0100
@@ -171,8 +171,8 @@
 
 exception Interrupt;
 
-fun ignore_interrupt f x = f x;
-fun raise_interrupt f x = f x;
+fun interruptible f x = f x;
+fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
 
 
 
diff -r abb3f8dd66dc -r a7475459c740 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;
 
diff -r abb3f8dd66dc -r a7475459c740 src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Sat Feb 16 16:44:02 2008 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Sat Feb 16 16:44:02 2008 +0100
@@ -275,8 +275,8 @@
 
 (** interrupts **)      (*Note: may get into race conditions*)
 
-fun ignore_interrupt f x = f x;
-fun raise_interrupt f x = f x;
+fun interruptible f x = f x;
+fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
 
 
 
diff -r abb3f8dd66dc -r a7475459c740 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Feb 16 16:44:02 2008 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Feb 16 16:44:02 2008 +0100
@@ -139,26 +139,35 @@
 
 exception Interrupt;
 
-fun ignore_interrupt f x =
+local
+
+fun change_signal new_handler f x =
   let
-    val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE);
-    val result = Exn.capture f x;
+    val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
+    val result = Exn.capture (f old_handler) x;
     val _ = Signals.setHandler (Signals.sigINT, old_handler);
   in Exn.release result end;
 
-fun raise_interrupt f x =
+in
+
+fun interruptible (f: 'a -> 'b) x =
   let
-    val interrupted = ref false;
-    val result = ref (Exn.Result ());
+    val result = ref (Exn.Exn Interrupt: 'b Exn.result);
     val old_handler = Signals.inqHandler Signals.sigINT;
   in
     SMLofNJ.Cont.callcc (fn cont =>
-      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont)));
-      result := Exn.capture f x));
+      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
+        result := Exn.capture f x));
     Signals.setHandler (Signals.sigINT, old_handler);
-    if ! interrupted then raise Interrupt else Exn.release (! result)
+    Exn.release (! result)
   end;
 
+fun uninterruptible f =
+  change_signal Signals.IGNORE
+    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
+
+end;
+
 
 (* basis library fixes *)