# HG changeset patch
# User wenzelm
# Date 1297177912 -3600
# Node ID 22f8c2483bd287516397988e9df763cc36671f9b
# Parent  3bafa8ba51db220faa6e782b76c016d97915ce26
explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;

diff -r 3bafa8ba51db -r 22f8c2483bd2 src/Pure/Concurrent/future.ML
--- 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;
diff -r 3bafa8ba51db -r 22f8c2483bd2 src/Pure/Isar/runtime.ML
--- 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 =>