# HG changeset patch
# User blanchet
# Date 1354537495 -3600
# Node ID dddcaeb92e112908e253b81a9409c9c7c6e4947c
# Parent  c192ba6e6e5d1bd457c64eb8542523404f59c8fd
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

diff -r c192ba6e6e5d -r dddcaeb92e11 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 02 22:20:12 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 03 13:24:55 2012 +0100
@@ -119,6 +119,7 @@
     xs |> chunk_list 500
        |> List.app (File.append path o space_implode "" o map f)
   end
+  handle IO.Io _ => ()
 
 fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
   let
@@ -204,9 +205,9 @@
 fun mash_CLEAR ctxt =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh CLEAR");
-    File.fold_dir (fn file => fn _ =>
-                      try File.rm (Path.append path (Path.basic file)))
-                  path NONE;
+    try (File.fold_dir (fn file => fn _ =>
+                           try File.rm (Path.append path (Path.basic file)))
+                       path) NONE;
     ()
   end