# 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);