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