src/Pure/ML-Systems/multithreading_polyml.ML
changeset 30602 1bd90b76477a
parent 29564 f8b933a62151
child 30612 cb6421b6a18f
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 09:52:32 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 11:08:59 2009 +0100
     1.3 @@ -77,11 +77,9 @@
     1.4  fun with_attributes new_atts f x =
     1.5    let
     1.6      val orig_atts = safe_interrupts (Thread.getAttributes ());
     1.7 -    fun restore () = Thread.setAttributes orig_atts;
     1.8 -    val result =
     1.9 -      (Thread.setAttributes (safe_interrupts new_atts);
    1.10 -        Exn.Result (f orig_atts x) before restore ())
    1.11 -      handle e => Exn.Exn e before restore ();
    1.12 +    val result = Exn.capture (fn () =>
    1.13 +      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
    1.14 +    val _ = Thread.setAttributes orig_atts;
    1.15    in Exn.release result end;
    1.16  
    1.17  fun interruptible f = with_attributes regular_interrupts (fn _ => f);