1.1 --- a/src/Pure/Concurrent/future.ML	Sat Mar 21 12:37:13 2009 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Mar 21 13:11:12 2009 +0100
     1.3 @@ -44,6 +44,7 @@
     1.4    val join_result: 'a future -> 'a Exn.result
     1.5    val join: 'a future -> 'a
     1.6    val map: ('a -> 'b) -> 'a future -> 'b future
     1.7 +  val interruptible_task: ('a -> 'b) -> 'a -> 'b
     1.8    val interrupt_task: string -> unit
     1.9    val cancel_group: group -> unit
    1.10    val cancel: 'a future -> unit
    1.11 @@ -350,6 +351,15 @@
    1.12  
    1.13  (* cancellation *)
    1.14  
    1.15 +fun interruptible_task f x =
    1.16 +  if Multithreading.available then
    1.17 +    Multithreading.with_attributes
    1.18 +      (if is_some (thread_data ())
    1.19 +       then Multithreading.restricted_interrupts
    1.20 +       else Multithreading.regular_interrupts)
    1.21 +      (fn _ => f) x
    1.22 +  else interruptible f x;
    1.23 +
    1.24  (*interrupt: permissive signal, may get ignored*)
    1.25  fun interrupt_task id = SYNCHRONIZED "interrupt"
    1.26    (fn () => Task_Queue.interrupt_external (! queue) id);

     2.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 21 12:37:13 2009 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 21 13:11:12 2009 +0100
     2.3 @@ -311,7 +311,7 @@
     2.4  fun controlled_execution f =
     2.5    f
     2.6    |> debugging
     2.7 -  |> interruptible;
     2.8 +  |> Future.interruptible_task;
     2.9  
    2.10  fun program f =
    2.11   (f