# HG changeset patch
# User wenzelm
# Date 1014928473 -3600
# Node ID 42ac77552dbfb29f63bcc20c26fd6093fb9b8cc4
# Parent  2112f9e337bba5de4ead89ef727760fadfa475a7
renamed mask_interrupt to ignore_interrupt;
renamed exhibit_interrupt to raise_interrupt;
tuned interrupt handling code;

diff -r 2112f9e337bb -r 42ac77552dbf src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Feb 28 21:32:46 2002 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Feb 28 21:34:33 2002 +0100
@@ -99,15 +99,10 @@
 
 local
 
-datatype 'a result =
-  Result of 'a |
-  Exn of exn;
+fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;
 
-fun capture f x = Result (f x) handle exn => Exn exn;
-
-fun release (Result x) = x
-  | release (Exn exn) = raise exn;
-
+fun release NONE = ()
+  | release (SOME exn) = raise exn;
 
 val sig_int = 2;
 
@@ -125,8 +120,8 @@
 
 val _ = Signal.signal (sig_int, default_handler);
 
-fun mask_interrupt f = change_signal Signal.SIG_IGN f;
-fun exhibit_interrupt f = change_signal default_handler f;
+fun ignore_interrupt f = change_signal Signal.SIG_IGN f;
+fun raise_interrupt f = change_signal default_handler f;
 
 end;