adding a global time limit to the values command

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 16:52:20 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:10 2010 +0200
@@ -1799,7 +1799,7 @@
         mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
     val thy = ProofContext.theory_of ctxt
     val (ts, statistics) =
-      case compilation of
+      (case compilation of
        (* Random =>
           fst (Predicate.yieldn k
           (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
@@ -1809,25 +1809,25 @@
           let
             val [nrandom, size, depth] = arguments
           in
-            rpair NONE (fst (DSequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
-              depth true))
+              depth true)) ())
           end
       | DSeq =>
-          rpair NONE (fst (DSequence.yieldn k
+          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              thy NONE DSequence.map t' []) (the_single arguments) true))
+              thy NONE DSequence.map t' []) (the_single arguments) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = (the_single arguments)
           in
-            rpair NONE (fst (Lazy_Sequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
               thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
-              t' [] depth)))
+              t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
           let
@@ -1835,27 +1835,28 @@
             val seed = Random_Engine.next_seed ()
           in
             if stats then
-              apsnd (SOME o accumulate) (split_list
-              (fst (Lazy_Sequence.yieldn k
+              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+              (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
-                    t' [] nrandom size seed depth))))
+                    t' [] nrandom size seed depth))) ()))
             else rpair NONE
-              (fst (Lazy_Sequence.yieldn k
+              (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   thy NONE 
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
-                    t' [] nrandom size seed depth)))
+                    t' [] nrandom size seed depth))) ())
           end
       | _ =>
-          rpair NONE (fst (Predicate.yieldn k
+          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
-              thy NONE Predicate.map t' [])))
+              thy NONE Predicate.map t' []))) ()))
+     handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;
 
 fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =