# HG changeset patch
# User haftmann
# Date 1194351170 -3600
# Node ID 30142fd3babfc6d9f52000f73b3767808c032883
# Parent  fc01c83a466d2ceccd07a72a0bb6d7c410f74178
autoquickcheck message

diff -r fc01c83a466d -r 30142fd3babf src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Nov 06 13:12:49 2007 +0100
+++ b/src/Pure/codegen.ML	Tue Nov 06 13:12:50 2007 +0100
@@ -992,16 +992,18 @@
     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 test state =
+      let val _ = Output.priority "Autoquickcheck..."
+      in case try (TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
+            (test_goal true (params, []) 1 assms)) state
+       of NONE => (Output.priority "...no counterexample found"; state)
+        | SOME NONE => (Output.priority "...no counterexample found"; state)
+        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
+            Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
+      end;
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
-    then
-      (case try (fn state =>
-          TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
-           (test_goal true (params, []) 1 assms) state) state of
-         SOME (cex as SOME _) =>
-           Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
-             Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
-       | _ => state)
+    then test state
     else state
   end;