# HG changeset patch
# User blanchet
# Date 1354661004 -3600
# Node ID 187ae76a17570d0e23451d1a6437a89962074991
# Parent  41f8f1f2e15d5fd6f238789c9cc5d33341d4a43d
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions

diff -r 41f8f1f2e15d -r 187ae76a1757 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 23:19:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 04 23:43:24 2012 +0100
@@ -297,7 +297,9 @@
 
 local
 
-val version = "*** MaSh 0.1 ***"
+val version = "*** MaSh version 20121204a ***"
+
+exception Too_New of unit
 
 fun extract_node line =
   case space_explode ":" line of
@@ -326,8 +328,12 @@
                update_fact_graph_node (name, kind)
                #> fold (add_edge_to name) parents
            val fact_G =
-             try_graph ctxt "loading state" Graph.empty (fn () =>
-                 Graph.empty |> version' = version ? fold add_node node_lines)
+             case string_ord (version', version) of
+               EQUAL =>
+               try_graph ctxt "loading state" Graph.empty (fn () =>
+                   fold add_node node_lines Graph.empty)
+             | LESS => Graph.empty (* can't parse old file *)
+             | GREATER => raise Too_New ()
          in
            trace_msg ctxt (fn () =>
                "Loaded fact graph (" ^ graph_info fact_G ^ ")");
@@ -367,12 +373,14 @@
 
 fun mash_map ctxt f =
   Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
+  handle Too_New () => ()
 
 fun mash_peek ctxt f =
-  Synchronized.change_result global_state (load ctxt #> `snd #>> f)
+  Synchronized.change_result global_state
+      (perhaps (try (load ctxt)) #> `snd #>> f)
 
 fun mash_get ctxt =
-  Synchronized.change_result global_state (load ctxt #> `snd)
+  Synchronized.change_result global_state (perhaps (try (load ctxt)) #> `snd)
 
 fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>