# HG changeset patch
# User blanchet
# Date 1357421492 -3600
# Node ID 518f0b5ef3d90d395a128b3af290459a71b7d7a6
# Parent  82dee320d34097ce7dfee88fa81a635c2cf8e77f
tap after, not before command invocation

diff -r 82dee320d340 -r 518f0b5ef3d9 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 ()