# 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 _ =