# HG changeset patch
# User blanchet
# Date 1644853308 -3600
# Node ID 3bcbc4d12916b6fba1c6e2698e31bcf2c10000af
# Parent  27c93bfb0016a2577d8bd235f1aa762e97c70d19
print outcome of Sledgehammer search in panel

diff -r 27c93bfb0016 -r 3bcbc4d12916 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Feb 14 16:34:56 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Feb 14 16:41:48 2022 +0100
@@ -367,7 +367,7 @@
         fun found_proof prover_name =
           if mode = Normal then
             (Synchronized.change found_proofs (fn n => n + 1);
-             (writeln_result |> the_default writeln) (prover_name ^ " found a proof..."))
+             (the_default writeln writeln_result) (prover_name ^ " found a proof..."))
           else
             ()
 
@@ -459,10 +459,11 @@
          handle Timeout.TIMEOUT _ => (SH_Timeout, ""))
         |> `(fn (outcome, message) =>
           (case outcome of
-            SH_Some _ => (print "QED"; true)
-          | SH_Unknown => (print message; false)
-          | SH_Timeout => (print "No proof found"; false)
-          | SH_None => (print (if message = "" then "No proof found" else "Error: " ^ message);
+            SH_Some _ => (the_default writeln writeln_result "QED"; true)
+          | SH_Unknown => (the_default writeln writeln_result message; false)
+          | SH_Timeout => (the_default writeln writeln_result "No proof found"; false)
+          | SH_None => (the_default writeln writeln_result
+                (if message = "" then "No proof found" else "Error: " ^ message);
               false)))
       end)