# HG changeset patch
# User desharna
# Date 1745497512 -7200
# Node ID a310d5b6c696ba1c00a18c1e11881e5ed2c83475
# Parent  c17936c7a5095a8c4ad2eb15908015b646561b8a
proper command message for Sledgehammer's proof methods

diff -r c17936c7a509 -r a310d5b6c696 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Apr 24 09:16:33 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Apr 24 14:25:12 2025 +0200
@@ -44,6 +44,7 @@
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome ord
+  val try_command_line : string -> play_outcome -> string -> string
   val one_line_proof_text : one_line_params -> string
 end;
 
diff -r c17936c7a509 -r a310d5b6c696 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Thu Apr 24 09:16:33 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Thu Apr 24 14:25:12 2025 +0200
@@ -84,25 +84,23 @@
       end
 
     val timer = Timer.startRealTimer ()
-    val out =
+    val (outcome, command) =
       (case run_try0 () of
-        NONE => SOME GaveUp
-      | SOME _ => NONE)
-      handle ERROR _ => SOME GaveUp
-           | Exn.Interrupt_Breakdown => SOME GaveUp
-           | Timeout.TIMEOUT _ => SOME TimedOut
+        NONE => (SOME GaveUp, "")
+      | SOME {command, ...} => (NONE, command))
+      handle ERROR _ => (SOME GaveUp, "")
+           | Exn.Interrupt_Breakdown => (SOME GaveUp, "")
+           | Timeout.TIMEOUT _ => (SOME TimedOut, "")
     val run_time = Timer.checkRealTimer timer
 
-    val (outcome, used_facts) =
-      (case out of
-        NONE => (found_something name; (NONE, map fst facts))
-      | some_failure => (some_failure, []))
+    val used_facts =
+      (case outcome of
+        NONE => (found_something name; map fst facts)
+      | SOME _ => [])
 
     val message = fn _ =>
       (case outcome of
-        NONE =>
-        one_line_proof_text ((map (apfst Pretty.str) used_facts, (meth_of name, Played run_time)),
-          proof_banner mode name, subgoal, subgoal_count)
+        NONE => try_command_line (proof_banner mode name) (Played run_time) command
       | SOME failure => string_of_atp_failure failure)
   in
     {outcome = outcome, used_facts = used_facts, used_from = facts,