# HG changeset patch
# User bulwahn
# Date 1300866629 -3600
# Node ID 5e236f6ef04f53c0bad62f8f8068a4a5542961d0
# Parent  b579e787b582e91745529698baed2f7d17681a62
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout

diff -r b579e787b582 -r 5e236f6ef04f src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Tue Mar 22 21:22:50 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Wed Mar 23 08:50:29 2011 +0100
@@ -36,6 +36,7 @@
 theorem "rev (xs @ ys) = rev ys @ rev xs"
   quickcheck[random, expect = no_counterexample]
   quickcheck[exhaustive, expect = no_counterexample]
+  quickcheck[exhaustive, size = 1000, timeout = 0.1]
   oops
 
 theorem "rev (xs @ ys) = rev xs @ rev ys"
diff -r b579e787b582 -r 5e236f6ef04f src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Tue Mar 22 21:22:50 2011 +0100
+++ b/src/Tools/quickcheck.ML	Wed Mar 23 08:50:29 2011 +0100
@@ -190,8 +190,8 @@
     val _ = check_test_term t
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0
-    fun excipit s =
-      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
+    fun excipit () =
+      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
     val (test_fun, comp_time) = cpu_time "quickcheck compilation"
       (fn () => mk_tester ctxt (t, eval_terms));
     fun with_size test_fun k reports =
@@ -219,7 +219,7 @@
             (Option.map (mk_result names eval_terms) result,
               ([exec_time, comp_time],
                if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
-          end) (fn () => error (excipit "ran out of time")) ()
+          end) (fn () => (Output.urgent_message (excipit ()); (NONE, ([comp_time], NONE)))) ()
   end;
 
 fun test_terms ctxt ts =
@@ -269,7 +269,7 @@
       else if (forall is_some test_funs) then
         limit ctxt (limit_time, is_interactive) (fn () =>
           (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
-          (fn () => error "Quickcheck ran out of time") ()
+          (fn () => (Output.urgent_message "Quickcheck ran out of time"; (NONE, ([comp_time], NONE)))) ()
       else
         error "Unexpectedly, testers of some cardinalities are executable but others are not"
     end