removing exception handling now that is caught at some other point;
tuned message
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Dec 01 22:14:35 2011 +0100
@@ -155,7 +155,7 @@
(* FIXME: why decrement size by one? *)
let
val _ =
- Quickcheck.message ctxt ("[Quickcheck-exhaustive] Test " ^
+ Quickcheck.message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
(if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
"cardinality: " ^ string_of_int card)
val (ts, timing) =
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Dec 01 22:14:35 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Dec 01 22:14:35 2011 +0100
@@ -405,9 +405,7 @@
fun iterate_and_collect (card, size) 0 report = (NONE, report)
| iterate_and_collect (card, size) j report =
let
- val (test_result, single_report) = apsnd Run (single_tester card size) handle Match =>
- (if Config.get ctxt Quickcheck.quiet then ()
- else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
+ val (test_result, single_report) = apsnd Run (single_tester card size)
val report = collect_single_report single_report report
in
case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
@@ -425,13 +423,7 @@
fun single_tester c s = compile c s |> Random_Engine.run
fun iterate (card, size) 0 = NONE
| iterate (card, size) j =
- let
- val result = single_tester card size handle Match =>
- (if Config.get ctxt Quickcheck.quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE)
- in
- case result of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
- end
+ case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q
in
fn [card, size] => (rpair NONE (iterate (card, size) iterations))
end