src/Pure/ML-Systems/multithreading_polyml.ML
changeset 29550 67ec51c032cb
parent 28555 d59712ee942c
child 29564 f8b933a62151
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jan 18 16:33:09 2009 +0100
     1.3 @@ -77,12 +77,12 @@
     1.4  
     1.5  fun with_attributes new_atts f x =
     1.6    let
     1.7 -    val orig_atts = Thread.getAttributes ();
     1.8 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
     1.9      fun restore () = Thread.setAttributes orig_atts;
    1.10      val result =
    1.11        (Thread.setAttributes (safe_interrupts new_atts);
    1.12          Exn.Result (f orig_atts x) before restore ())
    1.13 -      handle e => Exn.Exn e before restore ()
    1.14 +      handle e => Exn.Exn e before restore ();
    1.15    in Exn.release result end;
    1.16  
    1.17  fun interruptible f = with_attributes regular_interrupts (fn _ => f);