enable_interrupt is back!
authorwenzelm
Fri, 01 Mar 2002 11:55:45 +0100
changeset 12992 c2648d3e67a8
parent 12991 1bfa0670f592
child 12993 1b76cc7ffef7
enable_interrupt is back!
src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 28 21:37:28 2002 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Fri Mar 01 11:55:45 2002 +0100
@@ -125,6 +125,8 @@
       val _ = unchange ();
     in release result end;
 
+fun enable_interrupt f = change_mask interruptible unmask_signals mask_signals f;
+
 in
 
 fun ignore_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f;
@@ -142,7 +144,7 @@
     fun proceed cont =
       let
         val _ = set_handler cont;
-        val result = unmask_interrupt (capture f) x;
+        val result = enable_interrupt (capture f) x;
         val _ = reset_handler ();
       in release result end;
   in