# HG changeset patch
# User wenzelm
# Date 1297262923 -3600
# Node ID 1b225934c09d3441da5fad415bc44e36988b6ba3
# Parent  02978b058ca94b9ac08a796dd845019bf23eacff
tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;

diff -r 02978b058ca9 -r 1b225934c09d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Feb 09 08:42:23 2011 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Feb 09 15:48:43 2011 +0100
@@ -182,8 +182,8 @@
           if ok then
             Exn.capture (fn () =>
               Multithreading.with_attributes Multithreading.private_interrupts
-                (fn _ =>
-                  Position.setmp_thread_data pos e () before Multithreading.interrupted ())) ()
+                (fn _ => Position.setmp_thread_data pos e ()) before
+              Multithreading.interrupted ()) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;