future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;

--- a/src/Pure/Concurrent/future.ML	Fri Mar 20 20:05:51 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Fri Mar 20 20:20:09 2009 +0100
@@ -236,7 +236,7 @@
 fun future_job group (e: unit -> 'a) =
   let
     val result = ref (NONE: 'a Exn.result option);
-    val job = Multithreading.with_attributes (Thread.getAttributes ())
+    val job = Multithreading.with_attributes Multithreading.restricted_interrupts
       (fn _ => fn ok =>
         let
           val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;

--- a/src/Pure/ML-Systems/multithreading.ML	Fri Mar 20 20:05:51 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Fri Mar 20 20:20:09 2009 +0100
@@ -21,6 +21,7 @@
   val enabled: unit -> bool
   val no_interrupts: Thread.threadAttribute list
   val regular_interrupts: Thread.threadAttribute list
+  val restricted_interrupts: Thread.threadAttribute list
   val with_attributes: Thread.threadAttribute list ->
     (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
   val self_critical: unit -> bool
@@ -46,6 +47,9 @@
 val regular_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
+val restricted_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
 fun with_attributes _ f x = f [] x;
 
 

--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 20:05:51 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Mar 20 20:20:09 2009 +0100
@@ -69,6 +69,9 @@
 val regular_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
 
+val restricted_interrupts =
+  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
+
 val safe_interrupts = map
   (fn Thread.InterruptState Thread.InterruptAsynch =>
       Thread.InterruptState Thread.InterruptAsynchOnce