1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    getenv "ISABELLE_HOME_USER" ^ "/mash"
     1.5    |> tap (Isabelle_System.mkdir o Path.explode)
     1.6  val mash_state_dir = mash_model_dir
     1.7 -fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
     1.8 +fun mash_state_file () = mash_state_dir () ^ "/state"
     1.9  
    1.10  
    1.11  (*** Isabelle helpers ***)
    1.12 @@ -385,11 +385,11 @@
    1.13  
    1.14  (* more friendly than "try o File.rm" for those who keep the files open in their
    1.15     text editor *)
    1.16 -fun wipe_out file = File.write file ""
    1.17 +fun wipe_out_file file = File.write (Path.explode file) ""
    1.18  
    1.19 -fun write_file (xs, f) file =
    1.20 +fun write_file heading (xs, f) file =
    1.21    let val path = Path.explode file in
    1.22 -    wipe_out path;
    1.23 +    File.write path heading;
    1.24      xs |> chunk_list 500
    1.25         |> List.app (File.append path o space_implode "" o map f)
    1.26    end
    1.27 @@ -411,8 +411,8 @@
    1.28        mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
    1.29        " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
    1.30    in
    1.31 -    write_file ([], K "") sugg_file;
    1.32 -    write_file write_cmds cmd_file;
    1.33 +    write_file "" ([], K "") sugg_file;
    1.34 +    write_file "" write_cmds cmd_file;
    1.35      trace_msg ctxt (fn () => "Running " ^ command);
    1.36      Isabelle_System.bash command;
    1.37      read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
    1.38 @@ -422,8 +422,7 @@
    1.39             | SOME "" => "Done"
    1.40             | SOME s => "Error: " ^ elide_string 1000 s))
    1.41      |> not overlord
    1.42 -       ? tap (fn _ => List.app (wipe_out o Path.explode)
    1.43 -                               [err_file, sugg_file, cmd_file])
    1.44 +       ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
    1.45    end
    1.46  
    1.47  fun str_of_add (name, parents, feats, deps) =
    1.48 @@ -506,7 +505,7 @@
    1.49  
    1.50  fun load _ (state as (true, _)) = state
    1.51    | load ctxt _ =
    1.52 -    let val path = mash_state_path () in
    1.53 +    let val path = mash_state_file () |> Path.explode in
    1.54        (true,
    1.55         case try File.read_lines path of
    1.56           SOME (version' :: node_lines) =>
    1.57 @@ -531,15 +530,13 @@
    1.58  
    1.59  fun save ctxt {fact_G} =
    1.60    let
    1.61 -    val path = mash_state_path ()
    1.62 -    fun fact_line_for name parents =
    1.63 -      escape_meta name ^ ": " ^ escape_metas parents
    1.64 -    val append_fact = File.append path o suffix "\n" oo fact_line_for
    1.65 -    fun append_entry (name, ((), (parents, _))) () =
    1.66 -      append_fact name (Graph.Keys.dest parents)
    1.67 +    fun str_of_entry (name, parents) =
    1.68 +      escape_meta name ^ ": " ^ escape_metas parents ^ "\n"
    1.69 +    fun append_entry (name, ((), (parents, _))) =
    1.70 +      cons (name, Graph.Keys.dest parents)
    1.71 +    val entries = [] |> Graph.fold append_entry fact_G
    1.72    in
    1.73 -    File.write path (version ^ "\n");
    1.74 -    Graph.fold append_entry fact_G ();
    1.75 +    write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ());
    1.76      trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")")
    1.77    end
    1.78  
    1.79 @@ -559,7 +556,9 @@
    1.80  
    1.81  fun mash_unlearn ctxt =
    1.82    Synchronized.change global_state (fn _ =>
    1.83 -      (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
    1.84 +      (mash_CLEAR ctxt;
    1.85 +       wipe_out_file (mash_state_file ());
    1.86 +       (true, empty_state)))
    1.87  
    1.88  end
    1.89