# HG changeset patch
# User blanchet
# Date 1309179395 -7200
# Node ID 78c2f14b35df7bdb98807904d72fd2c897104739
# Parent  ebeda6275027a67dd9b072dcbfaf5560a4a6fe60
clarify minimizer output

diff -r ebeda6275027 -r 78c2f14b35df src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 27 14:56:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon Jun 27 14:56:35 2011 +0200
@@ -167,18 +167,17 @@
            Int.min (msecs, Time.toMilliseconds time + slack_msecs)
            |> Time.fromMilliseconds
          val facts = filter_used_facts used_facts facts
-         val (min_thms, {preplay, message, message_tail, ...}) =
+         val (min_facts, {preplay, message, message_tail, ...}) =
            if length facts >= Config.get ctxt binary_min_facts then
              binary_minimize (do_test new_timeout) facts
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)
-         val n = length min_thms
          val _ = print silent (fn () => cat_lines
-           ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
-            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
+           ["Minimized to " ^ n_facts used_facts] ^
+            (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
                0 => ""
-             | n => " (including " ^ string_of_int n ^ " chained)") ^ ".")
-       in (SOME min_thms, (preplay, message, message_tail)) end
+             | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
+       in (SOME min_facts, (preplay, message, message_tail)) end
      | {outcome = SOME TimedOut, preplay, ...} =>
        (NONE,
         (preplay,
diff -r ebeda6275027 -r 78c2f14b35df src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 27 14:56:35 2011 +0200
@@ -738,6 +738,10 @@
                   facts |> map untranslated_fact |> filter_used_facts used_facts
                         |> map snd
               in
+                (if mode = Minimize then
+                   Output.urgent_message "Preplaying proof..."
+                 else
+                   ());
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
                                     metis_reconstructors
               end,