partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
--- 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) ());