src/Pure/ML-Systems/smlnj.ML

 fun print_depth n =
  (Compiler.Control.Print.printDepth := n div 2;
   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;
 
 (*Finish timing and return string*)

     if verbose then show_output () else ()
   end;
 
 
 
+(** 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 *)
 
 (*execute Unix command which doesn't take any input from stdin and

 
 
 (* 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 _ => "";
 
 
 (* getenv *)