# HG changeset patch
# User blanchet
# Date 1403880770 -7200
# Node ID 1f49da059947b613d35cc79dc1ddaabb2b4919b7
# Parent  a68ae60c15049a239b4397608e8a30dfd0471e7f
reintroduced 'extra features' + only print message in verbose mode

diff -r a68ae60c1504 -r 1f49da059947 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 14:20:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 16:52:50 2014 +0200
@@ -1255,8 +1255,8 @@
 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
 
 val chained_feature_factor = 0.5 (* FUDGE *)
-val extra_feature_factor = 0.05 (* FUDGE *)
-val num_extra_feature_facts = 0 (* FUDGE *)
+val extra_feature_factor = 0.1 (* FUDGE *)
+val num_extra_feature_facts = 10 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
@@ -1683,8 +1683,8 @@
    and Try. *)
 val min_secs_for_learning = 15
 
-fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...}) prover max_facts
-    ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+fun relevant_facts ctxt (params as {verbose, overlord, learn, fact_filter, timeout, ...}) prover
+    max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   if not (subset (op =) (the_list fact_filter, fact_filters)) then
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
@@ -1697,9 +1697,12 @@
         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.");
+            (if verbose then
+               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.")
+             else
+               ());
             launch_thread timeout
               (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
           end