# HG changeset patch
# User wenzelm
# Date 1194796230 -3600
# Node ID e05b9fa43885cfe7a892661c31ee9c4dd4c7b528
# Parent  595da5b9854b8e2a843202ba547fee05d74928df
auto quickcheck: reduced messages;

diff -r 595da5b9854b -r e05b9fa43885 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Nov 11 16:50:29 2007 +0100
+++ b/src/Pure/codegen.ML	Sun Nov 11 16:50:30 2007 +0100
@@ -992,19 +992,17 @@
     val ctxt = Proof.context_of state;
     val assms = map term_of (Assumption.assms_of ctxt);
     val params = get_test_params (Proof.theory_of state);
-    fun report msg = (Output.priority ("Auto quickcheck: " ^ msg); state);
     fun test () =
       let
-        val _ = Output.priority "Auto quickcheck ...";
         val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
           (try (test_goal true (params, []) 1 assms)) state;
       in
         case res of
-          NONE => report "failed."
-        | SOME NONE => report "no counterexamples found."
+          NONE => state
+        | SOME NONE => state
         | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
             Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
-      end handle TimeLimit.TimeOut => report "timeout.";
+      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
     then test ()