# HG changeset patch
# User bulwahn
# Date 1322641275 -3600
# Node ID cf22004ad55d628f6a5a22d36fd8a061441cb598
# Parent  e2e928af750b6fd2afee66f2110a9afa55854304
adding more verbose messages to exhaustive quickcheck

diff -r e2e928af750b -r cf22004ad55d src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 30 09:21:11 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 30 09:21:15 2011 +0100
@@ -153,6 +153,10 @@
     fun test_card_size test_fun (card, size) =
       (* FIXME: why decrement size by one? *)
       let
+        val _ =
+          Quickcheck.message ctxt ("[Quickcheck-exhaustive] Test " ^
+            (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
+            "cardinality: " ^ string_of_int card)          
         val (ts, timing) =
           cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
             (fn () => fst (test_fun [card, size - 1]))