# HG changeset patch
# User wenzelm
# Date 910607124 -3600
# Node ID 6f3cb53502fa2f0260ae4914632a0d49d7288ce1
# Parent  b4d4a97df4380702e7e80828ed13d9285ce7bba3
smart interrupt handler;

diff -r b4d4a97df438 -r 6f3cb53502fa src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Nov 09 11:20:46 1998 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Mon Nov 09 11:25:24 1998 +0100
@@ -85,6 +85,74 @@
 
 
 
+(** interrupts **)
+
+local
+
+datatype 'a result =
+  Result of 'a |
+  Exn of exn;
+
+fun capture f x = Result (f x) handle exn => Exn exn;
+
+fun release (Result x) = x
+  | release (Exn exn) = raise exn;
+
+
+val sig_int = System.Signals.SIGINT;
+
+val interruptible = not o System.Signals.masked;
+fun mask_signals () = System.Signals.maskSignals true;
+fun unmask_signals () = System.Signals.maskSignals false;
+
+fun change_mask ok change unchange f x =
+  if ok () then f x
+  else
+    let
+      val _ = change ();
+      val result = capture f x;
+      val _ = unchange ();
+    in release result end;
+
+in
+
+
+(* mask / unmask interrupt *)
+
+fun mask_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f;
+fun unmask_interrupt f = change_mask interruptible unmask_signals mask_signals f;
+
+
+(* exhibit interrupt (via exception) *)
+
+exception Interrupt;
+
+fun exhibit_interrupt f x =
+  let
+    val orig_handler = System.Signals.inqHandler sig_int;
+    fun reset_handler () = (System.Signals.setHandler (sig_int, orig_handler); ());
+
+    val interrupted = ref false;
+
+    fun set_handler cont =
+      System.Signals.setHandler (sig_int, SOME (fn _ => (interrupted := true; cont)));
+
+    fun proceed cont =
+      let
+        val _ = set_handler cont;
+        val result = unmask_interrupt (capture f) x;
+        val _ = reset_handler ();
+      in release result end;
+  in
+    callcc proceed;
+    reset_handler ();
+    if ! interrupted then raise Interrupt else ()
+   end;
+
+end;
+
+
+
 (** OS related **)
 
 (* system command execution *)
@@ -125,7 +193,7 @@
 end;
 
 (*redefine to flush its output immediately -- temporary patch suggested
-  by Kim Dam Petersen*)		(* FIXME !? *)
+  by Kim Dam Petersen*)         (* FIXME !? *)
 val output = fn (s, t) => (output (s, t); flush_out s);
 
 
diff -r b4d4a97df438 -r 6f3cb53502fa src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Nov 09 11:20:46 1998 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Nov 09 11:25:24 1998 +0100
@@ -34,11 +34,10 @@
   Compiler.Control.Print.printLength := n);
 
 
-
-(** Compiler-independent timing functions **)
+(* compiler-independent timing functions *)
 
 (*Note start point for timing*)
-fun startTiming() = 
+fun startTiming() =
   let val CPUtimer = Timer.startCPUTimer();
       val time = Timer.checkCPUTimer(CPUtimer)
   in  (CPUtimer,time)  end;
@@ -99,6 +98,79 @@
 
 
 
+(** interrupts **)
+
+local
+
+datatype 'a result =
+  Result of 'a |
+  Exn of exn;
+
+fun capture f x = Result (f x) handle exn => Exn exn;
+
+fun release (Result x) = x
+  | release (Exn exn) = raise exn;
+
+
+val sig_int = Signals.sigINT;
+val sig_int_mask = Signals.MASK [Signals.sigINT];
+
+fun interruptible () =
+  (case Signals.masked () of
+    Signals.MASKALL => false
+  | Signals.MASK sigs => List.all (fn s => s <> sig_int) sigs);
+
+val mask_signals = Signals.maskSignals;
+val unmask_signals = Signals.unmaskSignals;
+
+fun change_mask ok change unchange f x =
+  if ok () then f x
+  else
+    let
+      val _ = change sig_int_mask;
+      val result = capture f x;
+      val _ = unchange sig_int_mask;
+    in release result end;
+
+in
+
+
+(* mask / unmask interrupt *)
+
+fun mask_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f;
+fun unmask_interrupt f = change_mask interruptible unmask_signals mask_signals f;
+
+
+(* exhibit interrupt (via exception) *)
+
+exception Interrupt;
+
+fun exhibit_interrupt f x =
+  let
+    val orig_handler = Signals.inqHandler sig_int;
+    fun reset_handler () = (Signals.setHandler (sig_int, orig_handler); ());
+
+    val interrupted = ref false;
+
+    fun set_handler cont =
+      Signals.setHandler (sig_int, Signals.HANDLER (fn _ => (interrupted := true; cont)));
+
+    fun proceed cont =
+      let
+        val _ = set_handler cont;
+        val result = unmask_interrupt (capture f) x;
+        val _ = reset_handler ();
+      in release result end;
+  in
+    SMLofNJ.Cont.callcc proceed;
+    reset_handler ();
+    if ! interrupted then raise Interrupt else ()
+   end;
+
+end;
+
+
+
 (** OS related **)
 
 (* system command execution *)
@@ -121,7 +193,7 @@
 (* file handling *)
 
 (*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""		(* FIXME !? *)
+fun file_info "" = ""           (* FIXME !? *)
   | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";