print outcome of Sledgehammer search in panel
authorblanchet
Mon, 14 Feb 2022 16:41:48 +0100
changeset 75076 3bcbc4d12916
parent 75075 27c93bfb0016
child 75077 32947e5c453d
child 75078 ec86cb2418e1
print outcome of Sledgehammer search in panel
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)