# HG changeset patch
# User wenzelm
# Date 1308863520 -7200
# Node ID de5c79682b569df3bed0c543969bd9ebeb0f0189
# Parent  80803078552e0bd34aecad1262233b193239675d
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!

diff -r 80803078552e -r de5c79682b56 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jun 23 23:05:38 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Jun 23 23:12:00 2011 +0200
@@ -454,7 +454,8 @@
 fun execute_work NONE = ()
   | execute_work (SOME (work, deps')) = (worker_joining (fn () => execute work); join_work deps')
 and join_work deps =
-  execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
+  Multithreading.with_attributes Multithreading.no_interrupts
+    (fn _ => execute_work (SYNCHRONIZED "join" (fn () => join_next deps)));
 
 in