# HG changeset patch
# User blanchet
# Date 1354402538 -3600
# Node ID b00eeb8e352eb5bbe2f8349cc1f7d3ea0ff80acd
# Parent  38870ee593112cad3cf5ab070735c089454ccf44
proper quoting of paths in MaSh

diff -r 38870ee59311 -r b00eeb8e352e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 01 22:47:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 01 23:55:38 2012 +0100
@@ -101,12 +101,12 @@
 val relearn_isarN = "relearn_isar"
 val relearn_atpN = "relearn_atp"
 
-fun mash_home () = getenv "ISABELLE_SLEDGEHAMMER_MASH"
+fun mash_script () = Path.explode "$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py"
 fun mash_model_dir () =
-  getenv "ISABELLE_HOME_USER" ^ "/mash"
-  |> tap (Isabelle_System.mkdir o Path.explode)
+  Path.explode "$ISABELLE_HOME_USER/mash"
+  |> tap Isabelle_System.mkdir
 val mash_state_dir = mash_model_dir
-fun mash_state_file () = mash_state_dir () ^ "/state"
+fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
 
 
 (*** Isabelle helpers ***)
@@ -446,8 +446,9 @@
       " --numberOfPredictions " ^ string_of_int max_suggs ^
       (if save then " --saveModel" else "")
     val command =
-      mash_home () ^ "/src/mash.py --quiet --outputDir " ^ mash_model_dir () ^
-      " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
+      Path.implode (mash_script ()) ^ " --quiet --outputDir " ^
+      Path.implode (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
+      " >& " ^ err_file
       |> tap (fn _ => trace_msg ctxt (fn () =>
              case try File.read (Path.explode err_file) of
                NONE => "Done"
@@ -478,7 +479,7 @@
   "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
 
 fun mash_CLEAR ctxt =
-  let val path = mash_model_dir () |> Path.explode in
+  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)))
@@ -552,7 +553,7 @@
 
 fun load _ (state as (true, _)) = state
   | load ctxt _ =
-    let val path = mash_state_file () |> Path.explode in
+    let val path = mash_state_file () in
       (true,
        case try File.read_lines path of
          SOME (version' :: node_lines) =>
@@ -591,7 +592,8 @@
           (NONE, fold (append_entry o Graph.get_entry fact_G) names [])
         | NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G [])
     in
-      write_file banner (entries, str_of_entry) (mash_state_file ());
+      write_file banner (entries, str_of_entry)
+                 (Path.implode (mash_state_file ()));
       trace_msg ctxt (fn () =>
           "Saved fact graph (" ^ graph_info fact_G ^
           (case dirty of