# HG changeset patch # User wenzelm # Date 1187283202 -7200 # Node ID a50cdc42798d84db549184fe835d2480881fce4a # Parent 3479a9fe73e0f630480d8c409ed71cbc25057c30 improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt; diff -r 3479a9fe73e0 -r a50cdc42798d src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu Aug 16 18:53:21 2007 +0200 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu Aug 16 18:53:22 2007 +0200 @@ -59,10 +59,11 @@ handle Interrupt => (restore (); Exn.Exn Interrupt)) end; -fun with_interrupt_state state = with_attributes [Thread.InterruptState state]; +fun uninterruptible f x = with_attributes + [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer] f x; -fun uninterruptible f x = with_interrupt_state Thread.InterruptDefer f x; -fun interruptible f x = with_interrupt_state Thread.InterruptAsynchOnce f x; +fun interruptible f x = with_attributes + [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce] f x; (* critical section -- may be nested within the same thread *) @@ -206,3 +207,6 @@ val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL; val CRITICAL = Multithreading.CRITICAL; +fun ignore_interrupt f = Multithreading.uninterruptible (fn _ => f); +fun raise_interrupt f = Multithreading.interruptible (fn _ => f); +