# HG changeset patch
# User bulwahn
# Date 1288034231 -7200
# Node ID b7aa93c10833229bd706736e456ae0a777213240
# Parent  abc45472e48afd9b9e4c9ec658cdcaa80f253fe2
adding a global fixed timeout to quickcheck

diff -r abc45472e48a -r b7aa93c10833 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Oct 25 21:17:10 2010 +0200
+++ b/src/Tools/quickcheck.ML	Mon Oct 25 21:17:11 2010 +0200
@@ -194,10 +194,12 @@
           val (result, new_report) = with_testers k testers
           val reports = ((k, new_report) :: reports)
         in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
-    val ((result, reports), exec_time) = cpu_time "quickcheck execution"
+    val ((result, reports), exec_time) =
+      TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => cpu_time "quickcheck execution"
       (fn () => apfst
          (fn result => case result of NONE => NONE
-        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
+        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
+      handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
   in
     (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
   end;