# HG changeset patch
# User blanchet
# Date 1377092091 -7200
# Node ID f92b24047fc7a13121a9318b6cc4cdc1cc6d5278
# Parent  ea1b62ed5a546f7ca23016a6123f58fa3c3f07f7
improved support for MaSh server

diff -r ea1b62ed5a54 -r f92b24047fc7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 15:18:06 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 15:34:51 2013 +0200
@@ -154,7 +154,7 @@
     val (temp_dir, serial) =
       if overlord then (getenv "ISABELLE_HOME_USER", "")
       else (getenv "ISABELLE_TMP", serial_string ())
-    val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
+    val log_file = temp_dir ^ "/mash_log" ^ serial
     val err_file = temp_dir ^ "/mash_err" ^ serial
     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
     val sugg_path = Path.explode sugg_file
@@ -254,7 +254,7 @@
 fun unlearn ctxt =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh unlearn");
-    run_mash_tool ctxt false [shutdown_server_arg] ([], K "");
+    run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ());
     try (File.fold_dir (fn file => fn _ =>
                            try File.rm (Path.append path (Path.basic file)))
                        path) NONE;