# HG changeset patch
# User blanchet
# Date 1513691487 -3600
# Node ID cb34f5f49a08007ed7916d2aa56360ea0a1f6be6
# Parent  341fbce5b26dcb0bd18f64ff9921abd19dd7fe70
have 'try0' display results faster

diff -r 341fbce5b26d -r cb34f5f49a08 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Dec 18 16:58:13 2017 +0100
+++ b/src/HOL/Tools/try0.ML	Tue Dec 19 14:51:27 2017 +0100
@@ -122,9 +122,15 @@
   let
     val st = Proof.map_contexts (silence_methods false) st;
     fun trd (_, _, t) = t;
-    fun par_map f =
-      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o apply2 trd)
-      else Par_List.get_some f #> the_list;
+    fun try_method method = method mode timeout_opt quad st;
+    fun get_message (_, command, ms) = "Found proof: " ^ Active.sendback_markup_command
+      ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^
+      " (" ^ time_string ms ^ ")";
+    val print_step = Option.map (tap (writeln o get_message));
+    val get_results =
+      if mode = Normal
+      then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 trd)
+      else Par_List.get_some try_method #> the_list;
   in
     if mode = Normal then
       "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
@@ -132,7 +138,7 @@
       |> writeln
     else
       ();
-    (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
+    (case get_results apply_methods of
       [] =>
       (if mode = Normal then writeln "No proof found" else (); (false, (noneN, [])))
     | xs as (name, command, _) :: _ =>