# HG changeset patch
# User blanchet
# Date 1377259448 -7200
# Node ID 1e9735cd27aa213c226306ccfbcef998347eacc9
# Parent  cbd3c7c48d2c58b78227391be0e07b1428bbffd2
better tracing + honor blocking better

diff -r cbd3c7c48d2c -r 1e9735cd27aa src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 23 13:30:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 23 14:04:08 2013 +0200
@@ -255,10 +255,12 @@
 struct
 
 fun shutdown ctxt overlord =
-  run_mash_tool ctxt overlord [shutdown_server_arg] true ([], K "") (K ())
+  (trace_msg ctxt (K "MaSh shutdown");
+   run_mash_tool ctxt overlord [shutdown_server_arg] true ([], K "") (K ()))
 
 fun save ctxt overlord =
-  run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ())
+  (trace_msg ctxt (K "MaSh save");
+   run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ()))
 
 fun unlearn ctxt overlord =
   let val path = mash_model_dir () in
@@ -1274,7 +1276,8 @@
    Sledgehammer and Try. *)
 val min_secs_for_learning = 15
 
-fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...})
+fun relevant_facts ctxt
+        (params as {overlord, blocking, 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
@@ -1288,7 +1291,8 @@
   else
     let
       fun maybe_launch_thread () =
-        if not (Async_Manager.has_running_threads MaShN) andalso
+        if not blocking andalso
+           not (Async_Manager.has_running_threads MaShN) andalso
            (timeout = NONE orelse
             Time.toSeconds (the timeout) >= min_secs_for_learning) then
           let