# HG changeset patch
# User blanchet
# Date 1401453786 -7200
# Node ID f810d15ae62509dbe3b44b24f35b650fef4c10e8
# Parent  4874411752fe41c9e6cebd109669146f4f6a3040
added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away

diff -r 4874411752fe -r f810d15ae625 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 14:43:06 2014 +0200
@@ -188,6 +188,7 @@
     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
     val cmd_path = Path.explode cmd_file
     val model_dir = File.shell_path (mash_state_dir ())
+
     val command =
       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
       \PYTHONDONTWRITEBYTECODE=y ./mash.py\
@@ -201,6 +202,7 @@
       " --predictions " ^ sugg_file ^
       (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
       (if background then " &" else "")
+
     fun run_on () =
       (Isabelle_System.bash command
        |> tap (fn _ =>
@@ -208,6 +210,7 @@
            "" => trace_msg ctxt (K "Done")
          | s => warning ("MaSh error: " ^ elide_string 1000 s)));
        read_suggs (fn () => try File.read_lines sugg_path |> these))
+
     fun clean_up () =
       if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
   in
@@ -558,6 +561,7 @@
     val feats' = map (apfst name_of_feature) feats
   in
     MaSh_Py.unlearn ctxt overlord;
+    OS.Process.sleep (seconds 2.0); (* hack *)
     MaSh_Py.query ctxt overlord max_suggs (learns, [], parents', feats')
     |> map (apfst fact_of_name)
   end