# HG changeset patch
# User blanchet
# Date 1657544622 -7200
# Node ID a65c4539dedbf77efa13780e104c2f7bbd4059a5
# Parent  f2e402a19530d1fa205338ac6839c5e6cf73fd19
milder Sledgehammer messages

diff -r f2e402a19530 -r a65c4539dedb src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jul 11 08:21:54 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jul 11 15:03:42 2022 +0200
@@ -266,7 +266,7 @@
       else
         (really_go ()
          handle
-           ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n")
+           ERROR msg => (SH_Unknown, fn () => "Warning: " ^ msg ^ "\n")
          | exn =>
            if Exn.is_interrupt exn then Exn.reraise exn
            else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
@@ -495,7 +495,7 @@
           | 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);
+                (if message = "" then "No proof found" else "Warning: " ^ message);
               false)))
       end)
 
diff -r f2e402a19530 -r a65c4539dedb src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jul 11 08:21:54 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jul 11 15:03:42 2022 +0200
@@ -234,7 +234,7 @@
           "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
           \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")")
      | {message, ...} => (NONE, (prefix "Prover error: " o message))))
-    handle ERROR msg => (NONE, fn _ => "Error: " ^ msg)
+    handle ERROR msg => (NONE, fn _ => "Warning: " ^ msg)
   end
 
 fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
diff -r f2e402a19530 -r a65c4539dedb src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Mon Jul 11 08:21:54 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Mon Jul 11 15:03:42 2022 +0200
@@ -51,7 +51,7 @@
     (case prover params problem slice of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
     | _ => NONE)
-    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+    handle ERROR message => (warning ("Warning: " ^ message ^ "\n"); NONE)
   end
 
 fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =