# HG changeset patch
# User wenzelm
# Date 1312979335 -7200
# Node ID 2d16c693d536e785f05689612dc910d341b82d4b
# Parent  058520fa03a8b4c5c36099767288dad943768b37
synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;

diff -r 058520fa03a8 -r 2d16c693d536 src/Pure/Concurrent/future.ML
--- 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;