equal
deleted
inserted
replaced
148 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
148 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
149 val cmd_path = Path.explode cmd_file |
149 val cmd_path = Path.explode cmd_file |
150 val core = |
150 val core = |
151 "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
151 "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
152 " --numberOfPredictions " ^ string_of_int max_suggs ^ |
152 " --numberOfPredictions " ^ string_of_int max_suggs ^ |
153 " --learnTheories --NBSinePrior" ^ |
153 " --NBSinePrior" (* --learnTheories *) ^ |
154 (if save then " --saveModel" else "") |
154 (if save then " --saveModel" else "") |
155 val command = |
155 val command = |
156 "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^ |
156 "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^ |
157 File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^ |
157 File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^ |
158 " >& " ^ err_file |
158 " >& " ^ err_file |