src/Tools/quickcheck.ML

--- a/src/Tools/quickcheck.ML	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Tools/quickcheck.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -6,16 +6,34 @@
 
 signature QUICKCHECK =
 sig
-  val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
-  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
   val auto: bool ref
   val auto_time_limit: int ref
+  val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
+    (string * term) list option
+  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
 end;
 
 structure Quickcheck : QUICKCHECK =
 struct
 
-open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
+(* preferences *)
+
+val auto = ref false;
+val auto_time_limit = ref 2500;
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+  (setmp auto true (fn () =>
+    Preferences.bool_pref auto
+      "auto-quickcheck"
+      "Whether to enable quickcheck automatically.") ());
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+    (Preferences.nat_pref auto_time_limit
+      "auto-quickcheck-time-limit"
+      "Time limit for automatic quickcheck (in milliseconds).");
+
 
 (* quickcheck configuration -- default parameters, test generators *)
 
@@ -140,7 +158,7 @@
 
 (* automatic testing *)
 
-fun test_goal_auto int state =
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
   let
     val ctxt = Proof.context_of state;
     val assms = map term_of (Assumption.all_assms_of ctxt);
@@ -161,12 +179,10 @@
     if int andalso !auto andalso not (!Toplevel.quiet)
     then test ()
     else state
-  end;
-
-val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
+  end));
 
 
-(* Isar interfaces *)
+(* Isar commands *)
 
 fun read_nat s = case (Library.read_int o Symbol.explode) s
  of (k, []) => if k >= 0 then k