equal
deleted
inserted
replaced
152 fun run_mash_tool ctxt overlord extra_args write_cmds read_suggs = |
152 fun run_mash_tool ctxt overlord extra_args write_cmds read_suggs = |
153 let |
153 let |
154 val (temp_dir, serial) = |
154 val (temp_dir, serial) = |
155 if overlord then (getenv "ISABELLE_HOME_USER", "") |
155 if overlord then (getenv "ISABELLE_HOME_USER", "") |
156 else (getenv "ISABELLE_TMP", serial_string ()) |
156 else (getenv "ISABELLE_TMP", serial_string ()) |
157 val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" |
157 val log_file = temp_dir ^ "/mash_log" ^ serial |
158 val err_file = temp_dir ^ "/mash_err" ^ serial |
158 val err_file = temp_dir ^ "/mash_err" ^ serial |
159 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
159 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
160 val sugg_path = Path.explode sugg_file |
160 val sugg_path = Path.explode sugg_file |
161 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
161 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
162 val cmd_path = Path.explode cmd_file |
162 val cmd_path = Path.explode cmd_file |
252 struct |
252 struct |
253 |
253 |
254 fun unlearn ctxt = |
254 fun unlearn ctxt = |
255 let val path = mash_model_dir () in |
255 let val path = mash_model_dir () in |
256 trace_msg ctxt (K "MaSh unlearn"); |
256 trace_msg ctxt (K "MaSh unlearn"); |
257 run_mash_tool ctxt false [shutdown_server_arg] ([], K ""); |
257 run_mash_tool ctxt false [shutdown_server_arg] ([], K "") (K ()); |
258 try (File.fold_dir (fn file => fn _ => |
258 try (File.fold_dir (fn file => fn _ => |
259 try File.rm (Path.append path (Path.basic file))) |
259 try File.rm (Path.append path (Path.basic file))) |
260 path) NONE; |
260 path) NONE; |
261 () |
261 () |
262 end |
262 end |