1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -314,21 +314,29 @@
     1.4    if overlord then (getenv "ISABELLE_HOME_USER", "")
     1.5    else (getenv "ISABELLE_TMP", serial_string ())
     1.6  
     1.7 -fun run_mash ctxt overlord (temp_dir, serial) core =
     1.8 +fun and_rm_files overlord flags files =
     1.9 +  if overlord then
    1.10 +    ""
    1.11 +  else
    1.12 +    " && rm -f" ^ flags ^ " -- " ^
    1.13 +    space_implode " " (map File.shell_quote files)
    1.14 +
    1.15 +fun run_mash ctxt overlord (temp_dir, serial) async core =
    1.16    let
    1.17      val log_file = temp_dir ^ "/mash_log" ^ serial
    1.18      val err_file = temp_dir ^ "/mash_err" ^ serial
    1.19      val command =
    1.20 -      mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
    1.21 -      " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
    1.22 +      "(" ^ mash_home () ^ "/mash --quiet --outputDir " ^ mash_state_dir () ^
    1.23 +      " --log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^
    1.24 +      and_rm_files overlord "" [log_file, err_file] ^
    1.25 +      (if async then " &" else "")
    1.26    in
    1.27 -    trace_msg ctxt (fn () => "Running " ^ command);
    1.28 +    trace_msg ctxt (fn () =>
    1.29 +        (if async then "Launching " else "Running ") ^ command);
    1.30      write_file ([], K "") log_file;
    1.31      write_file ([], K "") err_file;
    1.32      Isabelle_System.bash command;
    1.33 -    if overlord then ()
    1.34 -    else (map (File.rm o Path.explode) [log_file, err_file]; ());
    1.35 -    trace_msg ctxt (K "Done")
    1.36 +    if not async then trace_msg ctxt (K "Done") else ()
    1.37    end
    1.38  
    1.39  (* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast
    1.40 @@ -337,18 +345,17 @@
    1.41    let
    1.42      val info as (temp_dir, serial) = mash_info overlord
    1.43      val in_dir = temp_dir ^ "/mash_init" ^ serial
    1.44 -    val in_dir_path = in_dir |> Path.explode |> tap Isabelle_System.mkdir
    1.45 +                 |> tap (Path.explode #> Isabelle_System.mkdir)
    1.46    in
    1.47      write_file write_access (in_dir ^ "/mash_accessibility");
    1.48      write_file write_feats (in_dir ^ "/mash_features");
    1.49      write_file write_deps (in_dir ^ "/mash_dependencies");
    1.50 -    run_mash ctxt overlord info ("--init --inputDir " ^ in_dir);
    1.51 -    (* FIXME: temporary hack *)
    1.52 -    if overlord then ()
    1.53 -    else (Isabelle_System.bash ("rm -r -f " ^ File.shell_path in_dir_path); ())
    1.54 +    run_mash ctxt overlord info true
    1.55 +             ("--init --inputDir " ^ in_dir ^
    1.56 +              and_rm_files overlord " -r" [in_dir])
    1.57    end
    1.58  
    1.59 -fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
    1.60 +fun run_mash_commands ctxt overlord async save max_suggs write_cmds read_suggs =
    1.61    let
    1.62      val info as (temp_dir, serial) = mash_info overlord
    1.63      val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
    1.64 @@ -356,14 +363,12 @@
    1.65    in
    1.66      write_file ([], K "") sugg_file;
    1.67      write_file write_cmds cmd_file;
    1.68 -    run_mash ctxt overlord info
    1.69 +    run_mash ctxt overlord info async
    1.70               ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
    1.71                " --numberOfPredictions " ^ string_of_int max_suggs ^
    1.72 -              (if save then " --saveModel" else ""));
    1.73 +              (if save then " --saveModel" else "") ^
    1.74 +              (and_rm_files overlord "" [sugg_file, cmd_file]));
    1.75      read_suggs (fn () => File.read_lines (Path.explode sugg_file))
    1.76 -    |> tap (fn _ =>
    1.77 -               if overlord then ()
    1.78 -               else (map (File.rm o Path.explode) [sugg_file, cmd_file]; ()))
    1.79    end
    1.80  
    1.81  fun str_of_update (name, parents, feats, deps) =
    1.82 @@ -395,11 +400,11 @@
    1.83    | mash_ADD ctxt overlord upds =
    1.84      (trace_msg ctxt (fn () => "MaSh ADD " ^
    1.85           elide_string 1000 (space_implode " " (map #1 upds)));
    1.86 -     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
    1.87 +     run_mash_commands ctxt overlord true true 0 (upds, str_of_update) (K ()))
    1.88  
    1.89  fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
    1.90    (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
    1.91 -   run_mash_commands ctxt overlord false max_suggs
    1.92 +   run_mash_commands ctxt overlord false false max_suggs
    1.93         ([query], str_of_query)
    1.94         (fn suggs => snd (extract_query (List.last (suggs ()))))
    1.95     handle List.Empty => [])