# HG changeset patch
# User blanchet
# Date 1343050350 -7200
# Node ID 72a31418ff8d77912b0a26ad49e66b5bdd961de8
# Parent  f30eb5eb7927e264338584f8d07d54fe998b9c92
faster "save" operation

diff -r f30eb5eb7927 -r 72a31418ff8d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -106,7 +106,7 @@
   getenv "ISABELLE_HOME_USER" ^ "/mash"
   |> tap (Isabelle_System.mkdir o Path.explode)
 val mash_state_dir = mash_model_dir
-fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
+fun mash_state_file () = mash_state_dir () ^ "/state"
 
 
 (*** Isabelle helpers ***)
@@ -385,11 +385,11 @@
 
 (* more friendly than "try o File.rm" for those who keep the files open in their
    text editor *)
-fun wipe_out file = File.write file ""
+fun wipe_out_file file = File.write (Path.explode file) ""
 
-fun write_file (xs, f) file =
+fun write_file heading (xs, f) file =
   let val path = Path.explode file in
-    wipe_out path;
+    File.write path heading;
     xs |> chunk_list 500
        |> List.app (File.append path o space_implode "" o map f)
   end
@@ -411,8 +411,8 @@
       mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
       " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
   in
-    write_file ([], K "") sugg_file;
-    write_file write_cmds cmd_file;
+    write_file "" ([], K "") sugg_file;
+    write_file "" write_cmds cmd_file;
     trace_msg ctxt (fn () => "Running " ^ command);
     Isabelle_System.bash command;
     read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
@@ -422,8 +422,7 @@
            | SOME "" => "Done"
            | SOME s => "Error: " ^ elide_string 1000 s))
     |> not overlord
-       ? tap (fn _ => List.app (wipe_out o Path.explode)
-                               [err_file, sugg_file, cmd_file])
+       ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
   end
 
 fun str_of_add (name, parents, feats, deps) =
@@ -506,7 +505,7 @@
 
 fun load _ (state as (true, _)) = state
   | load ctxt _ =
-    let val path = mash_state_path () in
+    let val path = mash_state_file () |> Path.explode in
       (true,
        case try File.read_lines path of
          SOME (version' :: node_lines) =>
@@ -531,15 +530,13 @@
 
 fun save ctxt {fact_G} =
   let
-    val path = mash_state_path ()
-    fun fact_line_for name parents =
-      escape_meta name ^ ": " ^ escape_metas parents
-    val append_fact = File.append path o suffix "\n" oo fact_line_for
-    fun append_entry (name, ((), (parents, _))) () =
-      append_fact name (Graph.Keys.dest parents)
+    fun str_of_entry (name, parents) =
+      escape_meta name ^ ": " ^ escape_metas parents ^ "\n"
+    fun append_entry (name, ((), (parents, _))) =
+      cons (name, Graph.Keys.dest parents)
+    val entries = [] |> Graph.fold append_entry fact_G
   in
-    File.write path (version ^ "\n");
-    Graph.fold append_entry fact_G ();
+    write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ());
     trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
   end
 
@@ -559,7 +556,9 @@
 
 fun mash_unlearn ctxt =
   Synchronized.change global_state (fn _ =>
-      (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
+      (mash_CLEAR ctxt;
+       wipe_out_file (mash_state_file ());
+       (true, empty_state)))
 
 end