1.1 --- a/src/Tools/quickcheck.ML Thu Feb 10 18:44:39 2011 +0100
1.2 +++ b/src/Tools/quickcheck.ML Fri Feb 11 11:47:42 2011 +0100
1.3 @@ -161,6 +161,11 @@
1.4 val time = Time.toMilliseconds (#cpu (end_timing start))
1.5 in (Exn.release result, (description, time)) end
1.6
1.7 +fun limit ctxt is_interactive f exc () =
1.8 + TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f ()
1.9 + handle TimeLimit.TimeOut =>
1.10 + if is_interactive then exc () else raise TimeLimit.TimeOut
1.11 +
1.12 fun test_term ctxt is_interactive t =
1.13 let
1.14 val (names, t') = apfst (map fst) (prep_test_term t);
1.15 @@ -185,7 +190,7 @@
1.16 in
1.17 case test_fun of NONE => (NONE, ([comp_time], NONE))
1.18 | SOME test_fun =>
1.19 - TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
1.20 + limit ctxt is_interactive (fn () =>
1.21 let
1.22 val ((result, reports), exec_time) =
1.23 cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
1.24 @@ -193,9 +198,7 @@
1.25 (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
1.26 ([exec_time, comp_time],
1.27 if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
1.28 - end) ()
1.29 - handle TimeLimit.TimeOut =>
1.30 - if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
1.31 + end) (fn () => error (excipit "ran out of time")) ()
1.32 end;
1.33
1.34 (* FIXME: this function shows that many assumptions are made upon the generation *)
1.35 @@ -225,10 +228,9 @@
1.36 if (forall is_none test_funs) then
1.37 (NONE, ([comp_time], NONE))
1.38 else if (forall is_some test_funs) then
1.39 - TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
1.40 - (get_first test_card_size enumeration_card_size, ([comp_time], NONE))) ()
1.41 - handle TimeLimit.TimeOut =>
1.42 - if is_interactive then error ("Quickcheck ran out of time") else raise TimeLimit.TimeOut
1.43 + limit ctxt is_interactive (fn () =>
1.44 + (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
1.45 + (fn () => error "Quickcheck ran out of time") ()
1.46 else
1.47 error "Unexpectedly, testers of some cardinalities are executable but others are not"
1.48 end