1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
     1.3 @@ -138,6 +138,9 @@
     1.4  
     1.5  (*** Low-level communication with MaSh ***)
     1.6  
     1.7 +val save_models_arg = "--saveModels"
     1.8 +val shutdown_server_arg = "--shutdownServer"
     1.9 +
    1.10  fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
    1.11  
    1.12  fun write_file banner (xs, f) path =
    1.13 @@ -145,7 +148,7 @@
    1.14     xs |> chunk_list 500 |> List.app (File.append path o implode o map f))
    1.15    handle IO.Io _ => ()
    1.16  
    1.17 -fun run_mash_tool ctxt overlord write_cmds read_suggs =
    1.18 +fun run_mash_tool ctxt overlord extra_args write_cmds read_suggs =
    1.19    let
    1.20      val (temp_dir, serial) =
    1.21        if overlord then (getenv "ISABELLE_HOME_USER", "")
    1.22 @@ -165,6 +168,7 @@
    1.23        " --modelFile=" ^ model_dir ^ "/model.pickle" ^
    1.24        " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
    1.25        " --log " ^ log_file ^ " " ^ core ^
    1.26 +      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
    1.27        " >& " ^ err_file
    1.28      fun run_on () =
    1.29        (Isabelle_System.bash command
    1.30 @@ -216,8 +220,6 @@
    1.31  
    1.32  val encode_features = map encode_feature #> space_implode " "
    1.33  
    1.34 -val str_of_saveless_shutdown = "S\n"
    1.35 -
    1.36  fun str_of_learn (name, parents, feats, deps) =
    1.37    "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
    1.38    encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
    1.39 @@ -251,7 +253,7 @@
    1.40  fun unlearn ctxt =
    1.41    let val path = mash_model_dir () in
    1.42      trace_msg ctxt (K "MaSh unlearn");
    1.43 -    run_mash_tool ctxt false ([()], K str_of_saveless_shutdown);
    1.44 +    run_mash_tool ctxt false [shutdown_server_arg] ([], K "");
    1.45      try (File.fold_dir (fn file => fn _ =>
    1.46                             try File.rm (Path.append path (Path.basic file)))
    1.47                         path) NONE;
    1.48 @@ -262,17 +264,19 @@
    1.49    | learn ctxt overlord learns =
    1.50      (trace_msg ctxt (fn () => "MaSh learn " ^
    1.51           elide_string 1000 (space_implode " " (map #1 learns)));
    1.52 -     run_mash_tool ctxt overlord (learns, str_of_learn) (K ()))
    1.53 +     run_mash_tool ctxt overlord [save_models_arg] (learns, str_of_learn)
    1.54 +                   (K ()))
    1.55  
    1.56  fun relearn _ _ [] = ()
    1.57    | relearn ctxt overlord relearns =
    1.58      (trace_msg ctxt (fn () => "MaSh relearn " ^
    1.59           elide_string 1000 (space_implode " " (map #1 relearns)));
    1.60 -     run_mash_tool ctxt overlord (relearns, str_of_relearn) (K ()))
    1.61 +     run_mash_tool ctxt overlord [save_models_arg] (relearns, str_of_relearn)
    1.62 +                   (K ()))
    1.63  
    1.64 -fun query ctxt overlord max_suggs (query as (learns, hints, _, feats)) =
    1.65 +fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
    1.66    (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
    1.67 -   run_mash_tool ctxt overlord ([query], str_of_query max_suggs)
    1.68 +   run_mash_tool ctxt overlord [] ([query], str_of_query max_suggs)
    1.69         (fn suggs =>
    1.70             case suggs () of
    1.71               [] => []