future_job: more robust Exn.capture outside thread attribute change;
authorwenzelm
Wed, 22 Jul 2009 10:46:35 +0200
changeset 32109 ff3677972e3f
parent 32108 77094a0bbc3e
child 32110 eff525e07a31
future_job: more robust Exn.capture outside thread attribute change;
src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Jul 22 10:45:35 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Jul 22 10:46:35 2009 +0200
@@ -161,8 +161,9 @@
       let
         val res =
           if ok then
-            Multithreading.with_attributes Multithreading.restricted_interrupts
-              (fn _ => fn () => Exn.capture e ()) ()
+            Exn.capture
+              (Multithreading.with_attributes Multithreading.restricted_interrupts
+                (fn _ => fn () => e ())) ()
           else Exn.Exn Exn.Interrupt;
         val _ = result := SOME res;
       in