# HG changeset patch
# User wenzelm
# Date 1374949645 -7200
# Node ID 8db0db07bd96c367d7c0e65ea8001e90ffbb8d05
# Parent  7b396ef36af6a3ac6c2226d1b04c2d9e6e4e82ce
clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;

diff -r 7b396ef36af6 -r 8db0db07bd96 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jul 27 17:34:56 2013 +0200
+++ b/src/Pure/goal.ML	Sat Jul 27 20:27:25 2013 +0200
@@ -182,7 +182,7 @@
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
 
 fun stable_futures id =
-  not (Par_Exn.is_interrupted (Future.join_results (peek_futures id)));
+  not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id)));
 
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (_, groups, _) =>