# HG changeset patch
# User blanchet
# Date 1377069940 -7200
# Node ID b1907f6b3c86452044d7b906dfb1f0901ac39285
# Parent  e08a58161bf1e3b4be401665085e3e4eef0352ab
shutdown MaSh server

diff -r e08a58161bf1 -r b1907f6b3c86 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
@@ -216,6 +216,8 @@
 
 val encode_features = map encode_feature #> space_implode " "
 
+val str_of_saveless_shutdown = "S\n"
+
 fun str_of_learn (name, parents, feats, deps) =
   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
   encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
@@ -249,6 +251,7 @@
 fun unlearn ctxt =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh unlearn");
+    run_mash_tool ctxt false ([()], K str_of_saveless_shutdown);
     try (File.fold_dir (fn file => fn _ =>
                            try File.rm (Path.append path (Path.basic file)))
                        path) NONE;