# HG changeset patch # User wenzelm # Date 1289555889 -3600 # Node ID dc0d4d4a1aa16971b5d4eeaf656342025d35b300 # Parent da2c56aaaa68b4f8c8826662d592c419c5dc8fda Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation; diff -r da2c56aaaa68 -r dc0d4d4a1aa1 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Thu Nov 11 19:58:07 2010 +0100 +++ b/src/Pure/Concurrent/lazy.ML Fri Nov 12 10:58:09 2010 +0100 @@ -55,8 +55,9 @@ (case expr of SOME e => let - val res = restore_interrupts (fn () => Exn.capture e ()) (); - val _ = Future.fulfill_result x res; + val res0 = restore_interrupts (fn () => Exn.capture e ()) (); + val _ = Future.fulfill_result x res0; + val res = Future.join_result x; (*semantic race: some other threads might see the same interrupt, until there is a fresh start*) val _ =