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 ());