# HG changeset patch
# User wenzelm
# Date 1232292789 -3600
# Node ID 67ec51c032cbe0c3f70be2bbd1bf3ba931fa3347
# Parent  7187373c6cb1ff412cc01fd91a2af86a88950e71
with_attributes: make double sure that unsafe attributes are avoided;

diff -r 7187373c6cb1 -r 67ec51c032cb src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jan 18 16:33:09 2009 +0100
@@ -77,12 +77,12 @@
 
 fun with_attributes new_atts f x =
   let
-    val orig_atts = Thread.getAttributes ();
+    val orig_atts = safe_interrupts (Thread.getAttributes ());
     fun restore () = Thread.setAttributes orig_atts;
     val result =
       (Thread.setAttributes (safe_interrupts new_atts);
         Exn.Result (f orig_atts x) before restore ())
-      handle e => Exn.Exn e before restore ()
+      handle e => Exn.Exn e before restore ();
   in Exn.release result end;
 
 fun interruptible f = with_attributes regular_interrupts (fn _ => f);