explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;

--- a/src/Pure/Concurrent/future.ML	Tue Feb 08 14:28:15 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 08 16:11:52 2011 +0100
@@ -182,7 +182,8 @@
           if ok then
             Exn.capture (fn () =>
               Multithreading.with_attributes Multithreading.private_interrupts
-                (fn _ => Position.setmp_thread_data pos e ())) ()
+                (fn _ =>
+                  Position.setmp_thread_data pos e () before Multithreading.interrupted ())) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;

--- a/src/Pure/Isar/runtime.ML	Tue Feb 08 14:28:15 2011 +0100
+++ b/src/Pure/Isar/runtime.ML	Tue Feb 08 16:11:52 2011 +0100
@@ -106,10 +106,8 @@
       | exn as EXCURSION_FAIL _ => Exn.Exn exn))
   else f x;
 
-fun controlled_execution f =
-  f
-  |> debugging
-  |> Future.interruptible_task;
+fun controlled_execution f x =
+  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
 
 fun toplevel_error output_exn f x = f x
   handle exn =>