# HG changeset patch
# User blanchet
# Date 1403801840 -7200
# Node ID 085e85cc6eea42851ef5df17f66ff94143fb476c
# Parent  ba0fe0639bc8f76e83537591e9e9ebc5146b5235
tuned output

diff -r ba0fe0639bc8 -r 085e85cc6eea src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 16:41:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 18:57:20 2014 +0200
@@ -192,19 +192,12 @@
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
 
 fun string_of_facts facts =
-  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+  "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^
   (facts |> map (fst o fst) |> space_implode " ") ^ "."
 
 fun string_of_factss factss =
-  if forall (null o snd) factss then
-    "Found no relevant facts."
-  else
-    (case factss of
-      [(_, facts)] => string_of_facts facts
-    | _ =>
-      factss
-      |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
-      |> space_implode "\n\n")
+  if forall (null o snd) factss then "Found no relevant facts."
+  else cat_lines (map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) factss)
 
 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
     output_result i (fact_override as {only, ...}) minimize_command state =
diff -r ba0fe0639bc8 -r 085e85cc6eea src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 16:41:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 18:57:20 2014 +0200
@@ -1714,10 +1714,13 @@
     [("", [])]
   else
     let
-      fun maybe_launch_thread () =
+      fun maybe_launch_thread min_num_facts_to_learn =
         if not (Async_Manager.has_running_threads MaShN) andalso
            Time.toSeconds timeout >= min_secs_for_learning then
           let val timeout = time_mult learn_timeout_slack timeout in
+            Output.urgent_message ("Started MaShing through at least " ^
+              string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^
+              " in the background");
             launch_thread timeout
               (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
           end
@@ -1729,8 +1732,9 @@
           let
             val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt overlord I
             val is_in_access_G = is_fact_in_graph access_G o snd
+            val min_num_facts_to_learn = length facts - num_facts0
           in
-            if length facts - num_facts0 <= max_facts_to_learn_before_query then
+            if min_num_facts_to_learn <= max_facts_to_learn_before_query then
               (case length (filter_out is_in_access_G facts) of
                 0 => false
               | num_facts_to_learn =>
@@ -1739,9 +1743,9 @@
                    |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
                    true)
                 else
-                  (maybe_launch_thread (); false))
+                  (maybe_launch_thread num_facts_to_learn; false))
             else
-              (maybe_launch_thread (); false)
+              (maybe_launch_thread min_num_facts_to_learn; false)
           end
         else
           false