partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
authorwenzelm
Thu, 12 Apr 2012 11:28:36 +0200
changeset 47430 b254fdaf1973
parent 47429 ec64d94cbf9c
child 47431 d9dd4a9f18fc
partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Apr 12 10:13:33 2012 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Apr 12 11:28:36 2012 +0200
@@ -61,15 +61,15 @@
             SOME e =>
               let
                 val res0 = Exn.capture (restore_attributes e) ();
-                val res1 = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                val res2 = Future.join_result x;
-              in
+                val _ = Exn.capture (fn () => 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*)
-                if Exn.is_interrupt_exn res1 orelse Exn.is_interrupt_exn res2 then
-                  (Synchronized.change var (fn _ => Expr e); Exn.interrupt ())
-                else res2
-              end
+                val _ =
+                  if Exn.is_interrupt_exn res then
+                    Synchronized.change var (fn _ => Expr e)
+                  else ();
+              in res end
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
         end) ());