more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;

--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 12:03:44 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 12:51:14 2011 +0200
@@ -174,13 +174,14 @@
 (* cancellation primitives *)
 
 fun interruptible_task f x =
-  if Multithreading.available then
+  (if Multithreading.available then
     Multithreading.with_attributes
       (if is_some (worker_task ())
        then Multithreading.private_interrupts
        else Multithreading.public_interrupts)
       (fn _ => f x)
-  else interruptible f x;
+   else interruptible f x)
+  before Multithreading.interrupted ();
 
 fun cancel_now group = (*requires SYNCHRONIZED*)
   Task_Queue.cancel (! queue) group;
@@ -209,9 +210,9 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
-        val _ = Exn.capture Multithreading.interrupted ();
+        val test = Exn.capture Multithreading.interrupted ();
         val _ =
-          if ok then ()
+          if ok andalso not (Exn.is_interrupt_exn test) then ()
           else if cancel_now group then ()
           else cancel_later group;
         val _ = broadcast work_finished;
@@ -245,7 +246,7 @@
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
-  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
+  | SOME work => (worker_exec work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -431,8 +432,7 @@
               Multithreading.with_attributes
                 (if interrupts
                  then Multithreading.private_interrupts else Multithreading.no_interrupts)
-                (fn _ => Position.setmp_thread_data pos e ()) before
-              Multithreading.interrupted ()) ()
+                (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;

--- a/src/Pure/Isar/runtime.ML	Fri Aug 19 12:03:44 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Aug 19 12:51:14 2011 +0200
@@ -119,7 +119,7 @@
   else f x;
 
 fun controlled_execution f x =
-  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
+  (f |> debugging |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>