# HG changeset patch
# User blanchet
# Date 1381692986 -7200
# Node ID 6fefbaeccb63dd7c65f6b4edb311fe68a695618f
# Parent  0b58c15ad284aaca26f1f92bc9bafa91e6673923
more prominent MaSh errors

diff -r 0b58c15ad284 -r 6fefbaeccb63 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 ()