1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 19:59:01 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Oct 02 21:21:21 2008 +0200
     1.3 @@ -69,20 +69,20 @@
     1.4  val regular_interrupts =
     1.5    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
     1.6  
     1.7 +val safe_interrupts = map
     1.8 +  (fn Thread.InterruptState Thread.InterruptAsynch =>
     1.9 +      Thread.InterruptState Thread.InterruptAsynchOnce
    1.10 +    | x => x);
    1.11 +
    1.12  fun with_attributes new_atts f x =
    1.13    let
    1.14      val orig_atts = Thread.getAttributes ();
    1.15      fun restore () = Thread.setAttributes orig_atts;
    1.16 -  in
    1.17 -    Exn.release
    1.18 -    (*RACE for fully asynchronous interrupts!*)
    1.19 -    (let
    1.20 -        val _ = Thread.setAttributes new_atts;
    1.21 -        val result = Exn.capture (f orig_atts) x;
    1.22 -        val _ = restore ();
    1.23 -      in result end
    1.24 -      handle Exn.Interrupt => (restore (); Exn.Exn Exn.Interrupt))
    1.25 -  end;
    1.26 +    val result =
    1.27 +      (Thread.setAttributes (safe_interrupts new_atts);
    1.28 +        Exn.Result (f orig_atts x) before restore ())
    1.29 +      handle e => Exn.Exn e before restore ()
    1.30 +  in Exn.release result end;
    1.31  
    1.32  fun interruptible f = with_attributes regular_interrupts (fn _ => f);
    1.33  
    1.34 @@ -104,7 +104,6 @@
    1.35      val watchdog = Thread.fork (fn () =>
    1.36        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
    1.37  
    1.38 -    (*RACE! timeout signal vs. external Interrupt*)
    1.39      val result = Exn.capture (restore_attributes f) x;
    1.40      val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
    1.41