# HG changeset patch
# User blanchet
# Date 1355682184 -3600
# Node ID fae8b1d9f701984bb69eaedd61330c7ad94c33d7
# Parent  2019ca8dcbfa1ad0542b947aa2a8c489d82dcc45
tuning

diff -r 2019ca8dcbfa -r fae8b1d9f701 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 16 19:13:19 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 16 19:23:04 2012 +0100
@@ -370,24 +370,23 @@
 
 in
 
-fun mash_map ctxt f =
+fun map_state ctxt f =
   Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
   handle Too_New () => ()
 
-fun mash_peek ctxt f =
+fun peek_state ctxt f =
   Synchronized.change_result global_state
       (perhaps (try (load ctxt)) #> `snd #>> f)
 
-fun mash_get ctxt =
-  Synchronized.change_result global_state (perhaps (try (load ctxt)) #> `snd)
-
-fun mash_unlearn ctxt =
+fun clear_state ctxt =
   Synchronized.change global_state (fn _ =>
       (mash_CLEAR ctxt; (* also removes the state file *)
        (true, empty_state)))
 
 end
 
+val mash_unlearn = clear_state
+
 
 (*** Isabelle helpers ***)
 
@@ -762,7 +761,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val (fact_G, suggs) =
-      mash_peek ctxt (fn {fact_G, ...} =>
+      peek_state ctxt (fn {fact_G, ...} =>
           if Graph.is_empty fact_G then
             (fact_G, [])
           else
@@ -825,7 +824,7 @@
           val feats = features_of ctxt prover thy (Local, General) [t]
           val deps = used_ths |> map nickname_of
         in
-          mash_peek ctxt (fn {fact_G, ...} =>
+          peek_state ctxt (fn {fact_G, ...} =>
               let val parents = maximal_in_graph fact_G facts in
                 mash_ADD ctxt overlord [(name, parents, feats, deps)]
               end);
@@ -843,7 +842,7 @@
     val timer = Timer.startRealTimer ()
     fun next_commit_time () =
       Time.+ (Timer.checkRealTimer timer, commit_timeout)
-    val {fact_G, ...} = mash_get ctxt
+    val {fact_G, ...} = peek_state ctxt I
     val facts = facts |> sort (thm_ord o pairself snd)
     val (old_facts, new_facts) =
       facts |> List.partition (is_fact_in_graph fact_G)
@@ -894,7 +893,7 @@
              Output.urgent_message "Committing..."
            else
              ();
-           mash_map ctxt (do_commit (rev adds) reps flops);
+           map_state ctxt (do_commit (rev adds) reps flops);
            if not last andalso auto_level = 0 then
              let val num_proofs = length adds + length reps in
                "Learned " ^ string_of_int num_proofs ^ " " ^
@@ -1032,7 +1031,8 @@
   end
 
 fun is_mash_enabled () = (getenv "MASH" = "yes")
-fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
+fun mash_can_suggest_facts ctxt =
+  not (Graph.is_empty (#fact_G (peek_state ctxt I)))
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)