# HG changeset patch
# User blanchet
# Date 1284643696 -7200
# Node ID b1172d65dd282b34be077f4bef8e0ac581cadecc
# Parent  2416666e6f94820d29dc4b5a54163b0efa8cb35f
skip some "important" messages

diff -r 2416666e6f94 -r b1172d65dd28 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 15:16:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 15:28:16 2010 +0200
@@ -192,6 +192,10 @@
 
 (* generic TPTP-based provers *)
 
+(* Important messages are important but not so important that users want to see
+   them each time. *)
+val keep_every_nth_important_message = 10
+
 fun prover_fun auto atp_name
         {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
          known_failures, default_max_relevant, explicit_forall,
@@ -304,7 +308,12 @@
     val (conjecture_shape, axiom_names) =
       repair_conjecture_shape_and_theorem_names output conjecture_shape
                                                 axiom_names
-    val important_message = extract_important_message output
+    val important_message =
+      if Time.toSeconds (Time.now ())
+         mod keep_every_nth_important_message = 0 then
+        extract_important_message output
+      else
+        ""
     val banner = if auto then "Sledgehammer found a proof"
                  else "Try this command"
     val (message, used_thm_names) =