moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure

--- a/src/Tools/quickcheck.ML	Wed Mar 30 10:31:02 2011 +0200
+++ b/src/Tools/quickcheck.ML	Wed Mar 30 11:32:51 2011 +0200
@@ -239,9 +239,6 @@
     val current_result = Unsynchronized.ref empty_result 
     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)]);
-    val _ = add_timing comp_time current_result
     fun with_size test_fun k =
       if k > Config.get ctxt size then
         NONE
@@ -257,17 +254,24 @@
           case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
         end;
   in
-    case test_fun of NONE => !current_result
-      | SOME test_fun =>
-        limit ctxt (limit_time, is_interactive) (fn () =>
-          let
-            val (response, exec_time) =
-              cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
-            val _ = add_response names eval_terms response current_result
-            val _ = add_timing exec_time current_result
-          in
-            !current_result
-          end) (fn () => (message (excipit ()); !current_result)) ()
+    limit ctxt (limit_time, is_interactive) (fn () =>
+      let
+        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+          (fn () => mk_tester ctxt [(t, eval_terms)]);
+        val _ = add_timing comp_time current_result
+      in
+        case test_fun of NONE => !current_result
+          | SOME test_fun =>
+            let
+              val (response, exec_time) =
+                cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+              val _ = add_response names eval_terms response current_result
+              val _ = add_timing exec_time current_result
+            in
+              !current_result
+            end
+       end)
+     (fn () => (message (excipit ()); !current_result)) ()
   end;
 
 fun test_terms ctxt ts =
@@ -297,14 +301,12 @@
     val _ = map check_test_term ts'
     val names = Term.add_free_names (hd ts') []
     val Ts = map snd (Term.add_frees (hd ts') [])
-    val current_result = Unsynchronized.ref empty_result 
-    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
-    val _ = add_timing comp_time current_result
-    fun test_card_size (card, size) =
+    val current_result = Unsynchronized.ref empty_result
+    fun test_card_size test_fun (card, size) =
       (* FIXME: why decrement size by one? *)
       let
         val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-          (fn () => fst ((the test_fun) [card - 1, size - 1]))
+          (fn () => fst (test_fun [card - 1, size - 1]))
         val _ = add_timing timing current_result
       in
         Option.map (pair card) ts
@@ -317,18 +319,23 @@
         (* size does matter *)
         map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
         |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
-    in
-      case test_fun of
+  in
+    limit ctxt (limit_time, is_interactive) (fn () =>
+      let
+        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
+        val _ = add_timing comp_time current_result
+      in
+        case test_fun of
           NONE => !current_result
         | SOME test_fun =>
-        limit ctxt (limit_time, is_interactive) (fn () =>
           let
-            val _ = case get_first test_card_size enumeration_card_size of
+            val _ = case get_first (test_card_size test_fun) enumeration_card_size of
               SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
             | NONE => ()
-          in !current_result end)
-          (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
-    end
+          in !current_result end
+      end)
+      (fn () => (message "Quickcheck ran out of time"; !current_result)) ()
+  end
 
 fun get_finite_types ctxt =
   fst (chop (Config.get ctxt finite_type_size)