restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;

--- a/src/Pure/Concurrent/future.ML	Sat Mar 21 12:37:13 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Mar 21 13:11:12 2009 +0100
@@ -44,6 +44,7 @@
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
   val map: ('a -> 'b) -> 'a future -> 'b future
+  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val interrupt_task: string -> unit
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -350,6 +351,15 @@
 
 (* cancellation *)
 
+fun interruptible_task f x =
+  if Multithreading.available then
+    Multithreading.with_attributes
+      (if is_some (thread_data ())
+       then Multithreading.restricted_interrupts
+       else Multithreading.regular_interrupts)
+      (fn _ => f) x
+  else interruptible f x;
+
 (*interrupt: permissive signal, may get ignored*)
 fun interrupt_task id = SYNCHRONIZED "interrupt"
   (fn () => Task_Queue.interrupt_external (! queue) id);

--- a/src/Pure/Isar/toplevel.ML	Sat Mar 21 12:37:13 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 21 13:11:12 2009 +0100
@@ -311,7 +311,7 @@
 fun controlled_execution f =
   f
   |> debugging
-  |> interruptible;
+  |> Future.interruptible_task;
 
 fun program f =
  (f