# 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;