make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -400,9 +400,9 @@
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
         preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
-        message = K ""}, ~1)
-    val ({outcome, used_facts, run_time_in_msecs, preplay, message}
-         : Sledgehammer_Provers.prover_result,
+        message = K "", message_tail = ""}, ~1)
+    val ({outcome, used_facts, run_time_in_msecs, preplay, message,
+          message_tail} : Sledgehammer_Provers.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
         val _ = if is_appropriate_prop concl_t then ()
@@ -421,7 +421,7 @@
       handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
            | Fail "inappropriate" => failed ATP_Proof.Inappropriate
     val time_prover = run_time_in_msecs |> the_default ~1
-    val msg = message (preplay ())
+    val msg = message (preplay ()) ^ message_tail
   in
     case outcome of
       NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
@@ -515,8 +515,9 @@
       Sledgehammer_Minimize.minimize_facts prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
-    val (used_facts, (preplay, message)) = minimize st (these (!named_thms))
-    val msg = message (preplay ())
+    val (used_facts, (preplay, message, message_tail)) =
+      minimize st (these (!named_thms))
+    val msg = message (preplay ()) ^ message_tail
   in
     case used_facts of
       SOME named_thms' =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -16,7 +16,7 @@
     string -> params -> bool -> int -> int -> Proof.state
     -> ((string * locality) * thm list) list
     -> ((string * locality) * thm list) list option
-       * ((unit -> play) * (play -> string))
+       * ((unit -> play) * (play -> string) * string)
   val run_minimize :
     params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
 end;
@@ -167,7 +167,7 @@
            Int.min (msecs, Time.toMilliseconds time + slack_msecs)
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
-         val (min_thms, {preplay, message, ...}) =
+         val (min_thms, {preplay, message, message_tail, ...}) =
            if length facts >= Config.get ctxt binary_min_facts then
              binary_minimize (do_test new_timeout) facts
            else
@@ -178,17 +178,18 @@
             (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
                0 => ""
              | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
-       in (SOME min_thms, (preplay, message)) end
+       in (SOME min_thms, (preplay, message, message_tail)) end
      | {outcome = SOME TimedOut, preplay, ...} =>
        (NONE,
         (preplay,
          fn _ => "Timeout: You can increase the time limit using the \
                  \\"timeout\" option (e.g., \"timeout = " ^
-                 string_of_int (10 + msecs div 1000) ^ "\")."))
+                 string_of_int (10 + msecs div 1000) ^ "\").",
+         ""))
      | {preplay, message, ...} =>
-       (NONE, (preplay, prefix "Prover error: " o message)))
+       (NONE, (preplay, prefix "Prover error: " o message, "")))
     handle ERROR msg =>
-           (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg))
+           (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
   end
 
 fun run_minimize (params as {provers, ...}) i refs state =
@@ -207,8 +208,9 @@
            | prover :: _ =>
              (kill_provers ();
               minimize_facts prover params false i n state facts
-              |> (fn (_, (preplay, message)) =>
-                     Output.urgent_message (message (preplay ()))))
+              |> (fn (_, (preplay, message, message_tail)) =>
+                     message (preplay ()) ^ message_tail
+                     |> Output.urgent_message))
   end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -57,7 +57,8 @@
      used_facts: (string * locality) list,
      run_time_in_msecs: int option,
      preplay: unit -> play,
-     message: play -> string}
+     message: play -> string,
+     message_tail: string}
 
   type prover =
     params -> (string -> minimize_command) -> prover_problem -> prover_result
@@ -324,7 +325,8 @@
    used_facts: (string * locality) list,
    run_time_in_msecs: int option,
    preplay: unit -> play,
-   message: play -> string}
+   message: play -> string,
+   message_tail: string}
 
 type prover =
   params -> (string -> minimize_command) -> prover_problem -> prover_result
@@ -774,7 +776,7 @@
         extract_important_message output
       else
         ""
-    val (used_facts, preplay, message) =
+    val (used_facts, preplay, message, message_tail) =
       case outcome of
         NONE =>
         let
@@ -803,25 +805,23 @@
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command minimize_command name preplay,
                    subgoal, subgoal_count)
-              in
-                proof_text ctxt isar_proof isar_params one_line_params ^
-                (if verbose then
-                   "\nATP real CPU time: " ^
-                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
-                 else
-                   "") ^
-                (if important_message <> "" then
-                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
-                   important_message
-                 else
-                   "")
-              end)
+              in proof_text ctxt isar_proof isar_params one_line_params end,
+           (if verbose then
+              "\nATP real CPU time: " ^
+              string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+            else
+              "") ^
+           (if important_message <> "" then
+              "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+              important_message
+            else
+              ""))
         end
       | SOME failure =>
-        ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure)
+        ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in
     {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs,
-     preplay = preplay, message = message}
+     preplay = preplay, message = message, message_tail = message_tail}
   end
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
@@ -974,7 +974,7 @@
       smt_filter_loop ctxt name params state subgoal smt_filter facts
     val (used_facts, used_ths) = used_facts |> ListPair.unzip
     val outcome = outcome |> Option.map failure_from_smt_failure
-    val (preplay, message) =
+    val (preplay, message, message_tail) =
       case outcome of
         NONE =>
         (fn () =>
@@ -994,21 +994,19 @@
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command minimize_command name preplay,
                  subgoal, subgoal_count)
-            in
-              one_line_proof_text one_line_params ^
-              (if verbose then
-                 "\nSMT solver real CPU time: " ^
-                 string_from_time (Time.fromMilliseconds
-                                       (the run_time_in_msecs)) ^ "."
-               else
-                 "")
-            end)
+            in one_line_proof_text one_line_params end,
+         if verbose then
+           "\nSMT solver real CPU time: " ^
+           string_from_time (Time.fromMilliseconds
+                                 (the run_time_in_msecs)) ^ "."
+         else
+           "")
       | SOME failure =>
-        (K (Failed_to_Play Metis), fn _ => string_for_failure failure)
+        (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
   in
     {outcome = outcome, used_facts = used_facts,
      run_time_in_msecs = run_time_in_msecs, preplay = preplay,
-     message = message}
+     message = message, message_tail = message_tail}
   end
 
 fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
@@ -1032,13 +1030,15 @@
                       val one_line_params =
                          (play, proof_banner mode name, used_facts,
                           minimize_command name, subgoal, subgoal_count)
-                    in one_line_proof_text one_line_params end}
+                    in one_line_proof_text one_line_params end,
+       message_tail = ""}
     | play =>
       let
         val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
       in
         {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE,
-         preplay = K play, message = fn _ => string_for_failure failure}
+         preplay = K play, message = fn _ => string_for_failure failure,
+         message_tail = ""}
       end
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -76,7 +76,7 @@
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time_in_msecs, preplay,
-                         message} : prover_result) =
+                         message, message_tail} : prover_result) =
   if is_some outcome then
     result
   else
@@ -112,7 +112,7 @@
             end
         else
           ((false, name), preplay)
-      val (used_facts, (preplay, message)) =
+      val (used_facts, (preplay, message, _)) =
         if minimize then
           minimize_facts minimize_name params (not verbose) subgoal
                          subgoal_count state
@@ -120,7 +120,7 @@
                               (map (apsnd single o untranslated_fact) facts))
           |>> Option.map (map fst)
         else
-          (SOME used_facts, (preplay, message))
+          (SOME used_facts, (preplay, message, ""))
     in
       case used_facts of
         SOME used_facts =>
@@ -137,7 +137,7 @@
            ();
          {outcome = NONE, used_facts = used_facts,
           run_time_in_msecs = run_time_in_msecs, preplay = preplay,
-          message = message})
+          message = message, message_tail = message_tail})
       | NONE => result
     end
 
@@ -167,10 +167,10 @@
     fun really_go () =
       problem
       |> get_minimizing_prover ctxt mode name params minimize_command
-      |> (fn {outcome, preplay, message, ...} =>
+      |> (fn {outcome, preplay, message, message_tail, ...} =>
              (if outcome = SOME ATP_Proof.TimedOut then timeoutN
               else if is_some outcome then noneN
-              else someN, message o preplay))
+              else someN, fn () => message (preplay ()) ^ message_tail))
     fun go () =
       let
         val (outcome_code, message) =