# HG changeset patch # User wenzelm # Date 1296833387 -3600 # Node ID 430493d65cd25d9d6f53218181a344a188078805 # Parent f33d5a00c25d7bf29359f1072d1cd2005e53b79d Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts; diff -r f33d5a00c25d -r 430493d65cd2 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Thu Feb 03 20:13:49 2011 +0100 +++ b/src/Pure/Concurrent/lazy.ML Fri Feb 04 16:29:47 2011 +0100 @@ -43,7 +43,7 @@ (case peek (Lazy var) of SOME res => res | NONE => - uninterruptible (fn restore_interrupts => fn () => + uninterruptible (fn restore_attributes => fn () => let val (expr, x) = Synchronized.change_result var @@ -55,7 +55,7 @@ (case expr of SOME e => let - val res0 = restore_interrupts (fn () => Exn.capture e ()) (); + val res0 = Exn.capture (restore_attributes e) (); val _ = Future.fulfill_result x res0; val res = Future.join_result x; (*semantic race: some other threads might see the same @@ -65,7 +65,7 @@ Synchronized.change var (fn _ => Expr e) else (); in res end - | NONE => restore_interrupts (fn () => Future.join_result x) ()) + | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) end) ()); fun force r = Exn.release (force_result r);