# HG changeset patch
# User wenzelm
# Date 1203176636 -3600
# Node ID a58cc0cf41768ffbc734ac17db429d582ad3a6f7
# Parent  4fc74eb2842bddf4491e5f9556f547aa5c6111e1
setmp: uninterruptible;

diff -r 4fc74eb2842b -r a58cc0cf4176 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat Feb 16 16:43:54 2008 +0100
+++ b/src/Pure/library.ML	Sat Feb 16 16:43:56 2008 +0100
@@ -332,21 +332,24 @@
 
 (*temporarily set flag during execution*)
 fun setmp_noncritical flag value f x =
-  let
-    val orig_value = ! flag;
-    val _ = flag := value;
-    val result = Exn.capture f x;
-    val _ = flag := orig_value;
-  in Exn.release result end;
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_value = ! flag;
+      val _ = flag := value;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = flag := orig_value;
+    in Exn.release result end) ();
 
-fun setmp flag value f x = NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
+fun setmp flag value f x =
+  NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
 
 fun setmp_thread_data tag orig_data data f x =
-  let
-    val _ = Multithreading.put_data (tag, data);
-    val result = Exn.capture f x;
-    val _ = Multithreading.put_data (tag, orig_data);
-  in Exn.release result end;
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val _ = Multithreading.put_data (tag, data);
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = Multithreading.put_data (tag, orig_data);
+    in Exn.release result end) ();