# HG changeset patch
# User wenzelm
# Date 1014928366 -3600
# Node ID 2112f9e337bba5de4ead89ef727760fadfa475a7
# Parent  b6db96775e5204bcd1be3de06208f6002f471256
renamed mask_interrupt to ignore_interrupt;
renamed exhibit_interrupt to raise_interrupt;

diff -r b6db96775e52 -r 2112f9e337bb src/Pure/ML-Systems/mlworks.ML
--- a/src/Pure/ML-Systems/mlworks.ML	Thu Feb 28 21:31:47 2002 +0100
+++ b/src/Pure/ML-Systems/mlworks.ML	Thu Feb 28 21:32:46 2002 +0100
@@ -24,7 +24,7 @@
     let val max_stack = MLWorks.Internal.Runtime.Memory.max_stack_blocks
     in max_stack := (!max_stack * 3) div 2 + 5;
        print ("#### Increasing stack to " ^ Int.toString (64 * !max_stack) ^
-	      "KB\n")
+              "KB\n")
     end);
   MLWorks.Internal.Runtime.Memory.gc_message_level := 10;
   (*Is this of any use at all?*)
@@ -91,14 +91,14 @@
 
 
 
-(** interrupts **)	(*Note: may get into race conditions*)
+(** interrupts **)      (*Note: may get into race conditions*)
 
 exception Interrupt;
 
 MLWorks.Internal.Runtime.Event.interrupt_handler (fn () => raise Interrupt);
 
-fun mask_interrupt f x = f x;           
-fun exhibit_interrupt f x = f x;
+fun ignore_interrupt f x = f x;
+fun raise_interrupt f x = f x;
 
 
 
diff -r b6db96775e52 -r 2112f9e337bb src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Feb 28 21:31:47 2002 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Feb 28 21:32:46 2002 +0100
@@ -98,8 +98,8 @@
 
 exception Interrupt;
 
-fun mask_interrupt f x = f x;           
-fun exhibit_interrupt f x = f x;
+fun ignore_interrupt f x = f x;           
+fun raise_interrupt f x = f x;
 
 
 
diff -r b6db96775e52 -r 2112f9e337bb src/Pure/ML-Systems/polyml-3.x.ML
--- a/src/Pure/ML-Systems/polyml-3.x.ML	Thu Feb 28 21:31:47 2002 +0100
+++ b/src/Pure/ML-Systems/polyml-3.x.ML	Thu Feb 28 21:32:46 2002 +0100
@@ -84,8 +84,8 @@
 
 (** interrupts **)      (*Note: may get into race conditions*)
 
-fun mask_interrupt f x = f x;
-fun exhibit_interrupt f x = f x;
+fun ignore_interrupt f x = f x;
+fun raise_interrupt f x = f x;
 
 
 
diff -r b6db96775e52 -r 2112f9e337bb src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 28 21:31:47 2002 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 28 21:32:46 2002 +0100
@@ -96,6 +96,8 @@
 
 (** interrupts **)
 
+exception Interrupt;
+
 local
 
 datatype 'a result =
@@ -125,18 +127,9 @@
 
 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;
+fun ignore_interrupt f = change_mask (not o interruptible) mask_signals unmask_signals f;
 
-
-(* exhibit interrupt (via exception) *)
-
-exception Interrupt;
-
-fun exhibit_interrupt f x =
+fun raise_interrupt f x =
   let
     val orig_handler = System.Signals.inqHandler sig_int;
     fun reset_handler () = (System.Signals.setHandler (sig_int, orig_handler); ());