# HG changeset patch
# User bulwahn
# Date 1297421262 -3600
# Node ID dbd00d8a47843235c8689b783dea76d633f5f70f
# Parent  73389fcafb66ece2cbf62fc95a1d13f987855285
quickcheck invokes TimeLimit.timeLimit only in one separate function

diff -r 73389fcafb66 -r dbd00d8a4784 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Feb 10 18:44:39 2011 +0100
+++ b/src/Tools/quickcheck.ML	Fri Feb 11 11:47:42 2011 +0100
@@ -161,6 +161,11 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
+fun limit ctxt is_interactive f exc () =
+  TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f ()
+  handle TimeLimit.TimeOut =>
+    if is_interactive then exc () else raise TimeLimit.TimeOut
+
 fun test_term ctxt is_interactive t =
   let
     val (names, t') = apfst (map fst) (prep_test_term t);
@@ -185,7 +190,7 @@
   in
     case test_fun of NONE => (NONE, ([comp_time], NONE))
       | SOME test_fun =>
-        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
+        limit ctxt is_interactive (fn () =>
           let
             val ((result, reports), exec_time) =
               cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
@@ -193,9 +198,7 @@
             (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
               ([exec_time, comp_time],
                if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
-          end) ()
-        handle TimeLimit.TimeOut =>
-          if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
+          end) (fn () => error (excipit "ran out of time")) ()
   end;
 
 (* FIXME: this function shows that many assumptions are made upon the generation *)
@@ -225,10 +228,9 @@
       if (forall is_none test_funs) then
         (NONE, ([comp_time], NONE))
       else if (forall is_some test_funs) then
-        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
-          (get_first test_card_size enumeration_card_size, ([comp_time], NONE))) ()
-        handle TimeLimit.TimeOut =>
-          if is_interactive then error ("Quickcheck ran out of time") else raise TimeLimit.TimeOut
+        limit ctxt is_interactive (fn () =>
+          (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
+          (fn () => error "Quickcheck ran out of time") ()
       else
         error "Unexpectedly, testers of some cardinalities are executable but others are not"
     end