synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;

--- a/src/Pure/Concurrent/future.ML	Wed Aug 10 14:04:45 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 10 14:28:55 2011 +0200
@@ -197,6 +197,7 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
+        val _ = Exn.capture Multithreading.interrupted ();
         val _ =
           if ok then ()
           else if cancel_now group then ()
@@ -397,7 +398,8 @@
         | _ => reraise exn);
     val ok =
       (case the (Single_Assignment.peek result) of
-        Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
+        Exn.Exn exn =>
+          (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false)
       | Exn.Res _ => true);
   in ok end;