1.1 --- a/src/Tools/quickcheck.ML	Wed Oct 28 11:55:48 2009 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Wed Oct 28 17:43:43 2009 +0100
     1.3 @@ -7,10 +7,10 @@
     1.4  signature QUICKCHECK =
     1.5  sig
     1.6    val auto: bool Unsynchronized.ref
     1.7 -  val auto_time_limit: int Unsynchronized.ref
     1.8    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
     1.9      (string * term) list option
    1.10    val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
    1.11 +  val setup: theory -> theory
    1.12    val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
    1.13  end;
    1.14  
    1.15 @@ -20,20 +20,13 @@
    1.16  (* preferences *)
    1.17  
    1.18  val auto = Unsynchronized.ref false;
    1.19 -val auto_time_limit = Unsynchronized.ref 2500;
    1.20  
    1.21  val _ =
    1.22    ProofGeneralPgip.add_preference Preferences.category_tracing
    1.23    (setmp_CRITICAL auto true (fn () =>
    1.24      Preferences.bool_pref auto
    1.25        "auto-quickcheck"
    1.26 -      "Whether to enable quickcheck automatically.") ());
    1.27 -
    1.28 -val _ =
    1.29 -  ProofGeneralPgip.add_preference Preferences.category_tracing
    1.30 -    (Preferences.nat_pref auto_time_limit
    1.31 -      "auto-quickcheck-time-limit"
    1.32 -      "Time limit for automatic quickcheck (in milliseconds).");
    1.33 +      "Whether to run Quickcheck automatically.") ());
    1.34  
    1.35  
    1.36  (* quickcheck configuration -- default parameters, test generators *)
    1.37 @@ -159,28 +152,26 @@
    1.38  
    1.39  (* automatic testing *)
    1.40  
    1.41 -val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    1.42 -  let
    1.43 -    val ctxt = Proof.context_of state;
    1.44 -    val assms = map term_of (Assumption.all_assms_of ctxt);
    1.45 -    val Test_Params { size, iterations, default_type } =
    1.46 -      (snd o Data.get o Proof.theory_of) state;
    1.47 -    fun test () =
    1.48 -      let
    1.49 -        val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
    1.50 -          (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
    1.51 -      in
    1.52 -        case res of
    1.53 -          NONE => state
    1.54 -        | SOME NONE => state
    1.55 -        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
    1.56 -            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
    1.57 -      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
    1.58 -  in
    1.59 -    if int andalso !auto andalso not (!Toplevel.quiet)
    1.60 -    then test ()
    1.61 -    else state
    1.62 -  end));
    1.63 +fun auto_quickcheck state =
    1.64 +  if not (!auto) then
    1.65 +    (false, state)
    1.66 +  else
    1.67 +    let
    1.68 +      val ctxt = Proof.context_of state;
    1.69 +      val assms = map term_of (Assumption.all_assms_of ctxt);
    1.70 +      val Test_Params { size, iterations, default_type } =
    1.71 +        (snd o Data.get o Proof.theory_of) state;
    1.72 +      val res =
    1.73 +        try (test_goal true NONE size iterations default_type [] 1 assms) state;
    1.74 +    in
    1.75 +      case res of
    1.76 +        NONE => (false, state)
    1.77 +      | SOME NONE => (false, state)
    1.78 +      | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    1.79 +          Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
    1.80 +    end
    1.81 +
    1.82 +val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
    1.83  
    1.84  
    1.85  (* Isar commands *)
    1.86 @@ -251,4 +242,3 @@
    1.87  
    1.88  
    1.89  val auto_quickcheck = Quickcheck.auto;
    1.90 -val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;