# HG changeset patch
# User wenzelm
# Date 1223578395 -7200
# Node ID 003f52c2bb8fc48c3d93ab18b482ff2ada096f0d
# Parent  c81f6344bfb71d154d074d41a623d20bd680c970
future result: Interrupt invalidates group, but pretends success otherwise;

diff -r c81f6344bfb7 -r 003f52c2bb8f src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Oct 09 20:53:14 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 09 20:53:15 2008 +0200
@@ -242,12 +242,13 @@
       (fn _ => fn ok =>
         let
           val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
+          val _ = result := SOME res;
           val res_ok =
             (case res of
               Exn.Result _ => true
-            | Exn.Exn Exn.Interrupt => true
+            | Exn.Exn Exn.Interrupt => (TaskQueue.invalidate_group group; true)
             | _ => false);
-        in result := SOME res; res_ok end);
+        in res_ok end);
 
     val task = SYNCHRONIZED "future" (fn () =>
       change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());