--- a/src/Pure/ML-Systems/polyml_common.ML Tue Feb 08 17:27:18 2011 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Feb 08 17:36:21 2011 +0100
@@ -73,36 +73,6 @@
-(** interrupts **)
-
-local
-
-val sig_int = 2;
-val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
-
-val _ = Signal.signal (sig_int, default_handler);
-val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
-
-fun change_signal new_handler f x =
- let
- (*RACE wrt. other signals!*)
- val old_handler = Signal.signal (sig_int, new_handler);
- val result = Exn.capture (f old_handler) x;
- val _ = Signal.signal (sig_int, old_handler);
- in Exn.release result end;
-
-in
-
-fun interruptible f = change_signal default_handler (fn _ => f);
-
-fun uninterruptible f =
- change_signal Signal.SIG_IGN
- (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-
(** OS related **)
(* current directory *)