1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Aug 16 18:53:21 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Aug 16 18:53:22 2007 +0200
     1.3 @@ -59,10 +59,11 @@
     1.4        handle Interrupt => (restore (); Exn.Exn Interrupt))
     1.5    end;
     1.6  
     1.7 -fun with_interrupt_state state = with_attributes [Thread.InterruptState state];
     1.8 +fun uninterruptible f x = with_attributes
     1.9 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer] f x;
    1.10  
    1.11 -fun uninterruptible f x = with_interrupt_state Thread.InterruptDefer f x;
    1.12 -fun interruptible f x = with_interrupt_state Thread.InterruptAsynchOnce f x;
    1.13 +fun interruptible f x = with_attributes
    1.14 +  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce] f x;
    1.15  
    1.16  
    1.17  (* critical section -- may be nested within the same thread *)
    1.18 @@ -206,3 +207,6 @@
    1.19  val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
    1.20  val CRITICAL = Multithreading.CRITICAL;
    1.21  
    1.22 +fun ignore_interrupt f = Multithreading.uninterruptible (fn _ => f);
    1.23 +fun raise_interrupt f = Multithreading.interruptible (fn _ => f);
    1.24 +