src/Tools/quickcheck.ML
changeset 42087 5e236f6ef04f
parent 42032 143f37194911
child 42088 8d00484551fe
--- 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