Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid double 'Warning:' in Sledgehammer messages
authorblanchet
Wed, 01 Mar 2023 08:00:51 +0100
changeset 77426 4a6eb1b18340
parent 77425 bde374587d93
child 77427 4cdefee3f97f
avoid double 'Warning:' in Sledgehammer messages
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -334,10 +334,10 @@
       else
         (really_go ()
          handle
-           ERROR msg => (SH_Unknown, fn () => "Warning: " ^ msg ^ "\n")
+           ERROR msg => (SH_Unknown, fn () => msg ^ "\n")
          | exn =>
            if Exn.is_interrupt exn then Exn.reraise exn
-           else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+           else (SH_Unknown, fn () => Runtime.exn_message exn ^ "\n"))
 
     val (outcome, message) = Timeout.apply hard_timeout go ()
     val () = check_expected_outcome ctxt prover_name expect outcome
isabelle