src/Pure/ML-Systems/polyml.ML
changeset 26084 a7475459c740
parent 25732 308315ee2b6d
child 26215 94d32a7cd0fb
equal deleted inserted replaced
26083:abb3f8dd66dc 26084:a7475459c740
   139 exception Interrupt = SML90.Interrupt;
   139 exception Interrupt = SML90.Interrupt;
   140 
   140 
   141 local
   141 local
   142 
   142 
   143 val sig_int = 2;
   143 val sig_int = 2;
       
   144 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
       
   145 
       
   146 val _ = Signal.signal (sig_int, default_handler);
   144 
   147 
   145 fun change_signal new_handler f x =
   148 fun change_signal new_handler f x =
   146   let
   149   let
   147     (*RACE wrt. other signals*)
   150     (*RACE wrt. other signals!*)
   148     val old_handler = Signal.signal (sig_int, new_handler);
   151     val old_handler = Signal.signal (sig_int, new_handler);
   149     val result = Exn.capture f x;
   152     val result = Exn.capture (f old_handler) x;
   150     val _ = Signal.signal (sig_int, old_handler);
   153     val _ = Signal.signal (sig_int, old_handler);
   151   in Exn.release result end;
   154   in Exn.release result end;
   152 
   155 
   153 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
   156 in
   154 
   157 
   155 in
   158 fun interruptible f = change_signal default_handler (fn _ => f);
   156 
   159 
   157 val _ = Signal.signal (sig_int, default_handler);
   160 fun uninterruptible f =
   158 
   161   change_signal Signal.SIG_IGN
   159 fun ignore_interrupt f = change_signal Signal.SIG_IGN f;
   162     (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
   160 fun raise_interrupt f = change_signal default_handler f;
       
   161 
   163 
   162 end;
   164 end;
   163 
   165 
   164 
   166 
   165 
   167