# HG changeset patch
# User wenzelm
# Date 1374949708 -7200
# Node ID e4b8b2927a52caba0412f56397aa5431a6f2cb9d
# Parent  8db0db07bd96c367d7c0e65ea8001e90ffbb8d05# Parent  317663b422bb3e715225249fd1db13b6ffdb2661
merged;

diff -r 317663b422bb -r e4b8b2927a52 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Jul 27 18:02:41 2013 +0200
+++ b/src/Pure/System/options.scala	Sat Jul 27 20:28:28 2013 +0200
@@ -142,9 +142,12 @@
 
           if (get_option != "")
             java.lang.System.out.println(options.check_name(get_option).value)
-          else if (export_file != "")
+
+          if (export_file != "")
             File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
-          else java.lang.System.out.println(options.print)
+
+          if (get_option == "" && export_file == "")
+            java.lang.System.out.println(options.print)
 
           0
         case _ => error("Bad arguments:\n" + cat_lines(args))
diff -r 317663b422bb -r e4b8b2927a52 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jul 27 18:02:41 2013 +0200
+++ b/src/Pure/goal.ML	Sat Jul 27 20:28:28 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, _) =>