# HG changeset patch
# User desharna
# Date 1641212911 -3600
# Node ID 3f55c5feca58bb48cef6dea884f82322e378ea96
# Parent  340c5f3506a8e7c3e52720a667be1d159ac9b320
prefixed all mirabelle_sledgehammer output lines with sledgehammer output

diff -r 340c5f3506a8 -r 3f55c5feca58 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Dec 20 14:46:23 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Jan 03 13:28:31 2022 +0100
@@ -353,8 +353,7 @@
       | _ => "")
   in
     change_data (inc_sh_time_isa cpu_time);
-    Sledgehammer.short_string_of_sledgehammer_outcome sledgehamer_outcome ^ " " ^
-      triv_str ^ outcome_msg ^ msg
+    (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg)
   end
 
 end
@@ -472,7 +471,7 @@
             val trivial =
               check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle Timeout.TIMEOUT _ => false
-            val log1 =
+            val (outcome, log1) =
               run_sledgehammer change_data params output_dir e_selection_heuristic term_order
                 force_sos keep proof_method_from_msg theory_index trivial meth named_thms pos pre
             val log2 =
@@ -481,7 +480,11 @@
                 !meth ^ " (sledgehammer): " ^ run_proof_method change_data trivial false name meth
                   thms timeout pos pre
               | NONE => "")
-          in log1 ^ "\n" ^ log2 end
+          in
+            log1 ^ "\n" ^ log2
+            |> Symbol.trim_blanks
+            |> prefix_lines (Sledgehammer.short_string_of_sledgehammer_outcome outcome ^ " ")
+          end
       end
 
     fun finalize () = log_data (Synchronized.value data)