--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jan 05 22:31:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Jan 05 22:31:32 2013 +0100
@@ -152,13 +152,13 @@
"\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
File.shell_path (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"
- | SOME "" => "Done"
- | SOME s => "Error: " ^ elide_string 1000 s))
fun run_on () =
- (Isabelle_System.bash command;
+ (Isabelle_System.bash command
+ |> tap (fn _ => trace_msg ctxt (fn () =>
+ case try File.read (Path.explode err_file) of
+ NONE => "Done"
+ | SOME "" => "Done"
+ | SOME s => "Error: " ^ elide_string 1000 s));
read_suggs (fn () => try File.read_lines sugg_path |> these))
fun clean_up () =
if overlord then ()