src/Pure/codegen.ML
changeset 24805 34cbfb87dfe8
parent 24707 dfeb98f84e93
child 24867 e5b55d7be9bb
     1.1 --- a/src/Pure/codegen.ML	Mon Oct 01 21:19:52 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Oct 01 21:19:53 2007 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    val test_fn: (int -> (string * term) list option) ref
     1.5    val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
     1.6    val auto_quickcheck: bool ref
     1.7 -  val auto_quickcheck_time_limit: Time.time ref
     1.8 +  val auto_quickcheck_time_limit: int ref
     1.9    val eval_result: (unit -> term) ref
    1.10    val eval_term: theory -> term -> term
    1.11    val evaluation_conv: cterm -> thm
    1.12 @@ -986,7 +986,7 @@
    1.13              ProofContext.pretty_term ctxt t]) cex);
    1.14  
    1.15  val auto_quickcheck = ref true;
    1.16 -val auto_quickcheck_time_limit = ref (Time.fromSeconds 5);
    1.17 +val auto_quickcheck_time_limit = ref 5000;
    1.18  
    1.19  fun test_goal' int state =
    1.20    let
    1.21 @@ -996,14 +996,15 @@
    1.22    in
    1.23      if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
    1.24      then
    1.25 -      (case try (fn state => TimeLimit.timeLimit (!auto_quickcheck_time_limit)
    1.26 +      (case try (fn state =>
    1.27 +          TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
    1.28             (test_goal true (params, []) 1 assms) state) state of
    1.29           SOME (cex as SOME _) =>
    1.30             Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.31               Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
    1.32         | _ => state)
    1.33      else state
    1.34 -  end handle TimeLimit.TimeOut => state;
    1.35 +  end;
    1.36  
    1.37  val _ = Context.add_setup
    1.38    (Context.theory_map (Specification.add_theorem_hook test_goal'));
    1.39 @@ -1200,3 +1201,7 @@
    1.40    [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
    1.41  
    1.42  end;
    1.43 +
    1.44 +val auto_quickcheck = Codegen.auto_quickcheck;
    1.45 +val auto_quickcheck_time_limit = Codegen.auto_quickcheck_time_limit;
    1.46 +