--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 11 23:15:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Oct 13 21:36:26 2013 +0200
@@ -179,11 +179,10 @@
(if background then " &" else "")
fun run_on () =
(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));
+ |> tap (fn _ =>
+ case try File.read (Path.explode err_file) |> the_default "" of
+ "" => trace_msg ctxt (K "Done")
+ | s => warning ("MaSh error: " ^ elide_string 1000 s));
read_suggs (fn () => try File.read_lines sugg_path |> these))
fun clean_up () =
if overlord then ()