introduced Auto Nitpick in addition to Auto Quickcheck;
this required generalizing the theorem hook used by Quickcheck,
following a suggestion by Florian

--- a/doc-src/Nitpick/nitpick.tex	Wed Oct 28 11:55:48 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Oct 28 17:43:43 2009 +0100
@@ -112,6 +112,13 @@
 machine called \texttt{java}. The examples presented in this manual can be found
 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
 
+Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
+Nitpick also provides an automatic mode that can be enabled using the
+``Auto Nitpick'' option from the ``Isabelle'' menu in Proof General. In this
+mode, Nitpick is run on every newly entered theorem, much like Auto Quickcheck.
+The collective time limit for Auto Nitpick and Auto Quickcheck can be set using
+the ``Auto Counterexample Time Limit'' option.
+
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{nospam}}
 
@@ -154,16 +161,6 @@
 configured SAT solvers in Isabelle (e.g., for Refute), these will also be
 available to Nitpick.
 
-Throughout this manual, we will explicitly invoke the \textbf{nitpick} command.
-Nitpick also provides an automatic mode that can be enabled by specifying
-
-\prew
-\textbf{nitpick\_params} [\textit{auto}]
-\postw
-
-at the beginning of the theory file. In this mode, Nitpick is run for up to 5
-seconds (by default) on every newly entered theorem, much like Auto Quickcheck.
-
 \subsection{Propositional Logic}
 \label{propositional-logic}
 
@@ -1595,6 +1592,17 @@
 (\S\ref{authentication}), optimizations
 (\S\ref{optimizations}), and timeouts (\S\ref{timeouts}).
 
+You can instruct Nitpick to run automatically on newly entered theorems by
+enabling the ``Auto Nitpick'' option from the ``Isabelle'' menu in Proof
+General. For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation})
+and \textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
+\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
+disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
+\textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Counterexample
+Time Limit'' in Proof General's ``Isabelle'' menu. Nitpick's output is also more
+concise.
+
 The number of options can be overwhelming at first glance. Do not let that worry
 you: Nitpick's defaults have been chosen so that it almost always does the right
 thing, and the most important options have been covered in context in
@@ -1622,35 +1630,19 @@
 \end{enum}
 
 Default values are indicated in square brackets. Boolean options have a negated
-counterpart (e.g., \textit{auto} vs.\ \textit{no\_auto}). When setting Boolean
-options, ``= \textit{true}'' may be omitted.
+counterpart (e.g., \textit{blocking} vs.\ \textit{no\_blocking}). When setting
+Boolean options, ``= \textit{true}'' may be omitted.
 
 \subsection{Mode of Operation}
 \label{mode-of-operation}
 
 \begin{enum}
-\opfalse{auto}{no\_auto}
-Specifies whether Nitpick should be run automatically on newly entered theorems.
-For automatic runs, \textit{user\_axioms} (\S\ref{mode-of-operation}) and
-\textit{assms} (\S\ref{mode-of-operation}) are implicitly enabled,
-\textit{blocking} (\S\ref{mode-of-operation}), \textit{verbose}
-(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}) are
-disabled, \textit{max\_potential} (\S\ref{output-format}) is taken to be 0, and
-\textit{auto\_timeout} (\S\ref{timeouts}) is used as the time limit instead of
-\textit{timeout} (\S\ref{timeouts}). The output is also more concise.
-
-\nopagebreak
-{\small See also \textit{auto\_timeout} (\S\ref{timeouts}).}
-
 \optrue{blocking}{non\_blocking}
 Specifies whether the \textbf{nitpick} command should operate synchronously.
 The asynchronous (non-blocking) mode lets the user start proving the putative
 theorem while Nitpick looks for a counterexample, but it can also be more
 confusing. For technical reasons, automatic runs currently always block.
 
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
 \optrue{falsify}{satisfy}
 Specifies whether Nitpick should look for falsifying examples (countermodels) or
 satisfying examples (models). This manual assumes throughout that
@@ -1670,16 +1662,15 @@
 considered.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{assms}
-(\S\ref{mode-of-operation}), and \textit{debug} (\S\ref{output-format}).}
+{\small See also \textit{assms} (\S\ref{mode-of-operation}) and \textit{debug}
+(\S\ref{output-format}).}
 
 \optrue{assms}{no\_assms}
 Specifies whether the relevant assumptions in structured proof should be
 considered. The option is implicitly enabled for automatic runs.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{user\_axioms} (\S\ref{mode-of-operation}).}
+{\small See also \textit{user\_axioms} (\S\ref{mode-of-operation}).}
 
 \opfalse{overlord}{no\_overlord}
 Specifies whether Nitpick should put its temporary files in
@@ -1861,9 +1852,6 @@
 option is useful to determine which scopes are tried or which SAT solver is
 used. This option is implicitly disabled for automatic runs.
 
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
-
 \opfalse{debug}{no\_debug}
 Specifies whether Nitpick should display additional debugging information beyond
 what \textit{verbose} already displays. Enabling \textit{debug} also enables
@@ -1871,8 +1859,8 @@
 option is implicitly disabled for automatic runs.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}), \textit{overlord}
-(\S\ref{mode-of-operation}), and \textit{batch\_size} (\S\ref{optimizations}).}
+{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
+\textit{batch\_size} (\S\ref{optimizations}).}
 
 \optrue{show\_skolems}{hide\_skolem}
 Specifies whether the values of Skolem constants should be displayed as part of
@@ -1910,8 +1898,7 @@
 enabled.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}),
-\textit{check\_potential} (\S\ref{authentication}), and
+{\small See also \textit{check\_potential} (\S\ref{authentication}) and
 \textit{sat\_solver} (\S\ref{optimizations}).}
 
 \opt{max\_genuine}{int}{$\mathbf{1}$}
@@ -1968,8 +1955,7 @@
 shown to be genuine, Nitpick displays a message to this effect and terminates.
 
 \nopagebreak
-{\small See also \textit{max\_potential} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_potential} (\S\ref{output-format}).}
 
 \opfalse{check\_genuine}{trust\_genuine}
 Specifies whether genuine and likely genuine counterexamples should be given to
@@ -1979,8 +1965,7 @@
 \texttt{blan{\color{white}nospam}\kern-\wd\boxA{}[e-mail]}.
 
 \nopagebreak
-{\small See also \textit{max\_genuine} (\S\ref{output-format}) and
-\textit{auto\_timeout} (\S\ref{timeouts}).}
+{\small See also \textit{max\_genuine} (\S\ref{output-format}).}
 
 \ops{expect}{string}
 Specifies the expected outcome, which must be one of the following:
@@ -2206,19 +2191,12 @@
 Specifies the maximum amount of time that the \textbf{nitpick} command should
 spend looking for a counterexample. Nitpick tries to honor this constraint as
 well as it can but offers no guarantees. For automatic runs,
-\textit{auto\_timeout} is used instead.
+\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
+a time slot whose length is specified by the ``Auto Counterexample Time
+Limit'' option in Proof General.
 
 \nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation})
-and \textit{max\_threads} (\S\ref{optimizations}).}
-
-\opt{auto\_timeout}{time}{$\mathbf{5}$ s}
-Specifies the maximum amount of time that Nitpick should use to find a
-counterexample when running automatically. Nitpick tries to honor this
-constraint as well as it can but offers no guarantees.
-
-\nopagebreak
-{\small See also \textit{auto} (\S\ref{mode-of-operation}).}
+{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
 
 \opt{tac\_timeout}{time}{$\mathbf{500}$\,ms}
 Specifies the maximum amount of time that the \textit{auto} tactic should use

--- a/src/HOL/IsaMakefile	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Oct 28 17:43:43 2009 +0100
@@ -101,6 +101,7 @@
   $(SRC)/Provers/hypsubst.ML \
   $(SRC)/Provers/quantifier1.ML \
   $(SRC)/Provers/splitter.ML \
+  $(SRC)/Tools/Auto_Counterexample.thy \
   $(SRC)/Tools/Code/code_haskell.ML \
   $(SRC)/Tools/Code/code_ml.ML \
   $(SRC)/Tools/Code/code_preproc.ML \
@@ -113,6 +114,7 @@
   $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   $(SRC)/Tools/IsaPlanner/zipper.ML \
   $(SRC)/Tools/atomize_elim.ML \
+  $(SRC)/Tools/auto_counterexample.ML \
   $(SRC)/Tools/auto_solve.ML \
   $(SRC)/Tools/coherent.ML \
   $(SRC)/Tools/cong_tac.ML \

--- a/src/HOL/Main.thy	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Main.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Nitpick Quickcheck Recdef
+imports Plain Nitpick
 begin
 
 text {*

--- a/src/HOL/Nitpick.thy	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Nitpick.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports Map SAT
+imports Map Quickcheck SAT
 uses ("Tools/Nitpick/kodkod.ML")
      ("Tools/Nitpick/kodkod_sat.ML")
      ("Tools/Nitpick/nitpick_util.ML")
@@ -241,6 +241,8 @@
 use "Tools/Nitpick/nitpick_tests.ML"
 use "Tools/Nitpick/minipick.ML"
 
+setup {* Nitpick_Isar.setup *}
+
 hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim 
     bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
     fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac

--- a/src/HOL/Quickcheck.thy	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Quickcheck.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -126,6 +126,8 @@
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
+setup {* Quickcheck.setup *}
+
 use "Tools/quickcheck_generators.ML"
 setup {* Quickcheck_Generators.setup *}
 

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 17:43:43 2009 +0100
@@ -187,7 +187,7 @@
     val pprint =
       if auto then
         Unsynchronized.change state_ref o Proof.goal_message o K
-        o curry Pretty.blk 0 o cons (Pretty.str "") o single
+        o Pretty.chunks o cons (Pretty.str "") o single
         o Pretty.mark Markup.hilite
       else
         priority o Pretty.string_of

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 17:43:43 2009 +0100
@@ -10,7 +10,9 @@
 sig
   type params = Nitpick.params
 
+  val auto: bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
+  val setup : theory -> theory
 end
 
 structure Nitpick_Isar : NITPICK_ISAR =
@@ -22,6 +24,14 @@
 open Nitpick_Nut
 open Nitpick
 
+val auto = Unsynchronized.ref false;
+
+val _ = ProofGeneralPgip.add_preference Preferences.category_tracing
+            (setmp_CRITICAL auto false
+                 (fn () => Preferences.bool_pref auto
+                               "auto-nitpick"
+                               "Whether to run Nitpick automatically.") ())
+
 type raw_param = string * string list
 
 val default_default_params =
@@ -33,7 +43,6 @@
    ("wf", ["smart"]),
    ("sat_solver", ["smart"]),
    ("batch_size", ["smart"]),
-   ("auto", ["false"]),
    ("blocking", ["true"]),
    ("falsify", ["true"]),
    ("user_axioms", ["smart"]),
@@ -47,7 +56,6 @@
    ("fast_descrs", ["true"]),
    ("peephole_optim", ["true"]),
    ("timeout", ["30 s"]),
-   ("auto_timeout", ["5 s"]),
    ("tac_timeout", ["500 ms"]),
    ("sym_break", ["20"]),
    ("sharing_depth", ["3"]),
@@ -70,7 +78,6 @@
   [("dont_box", "box"),
    ("non_mono", "mono"),
    ("non_wf", "wf"),
-   ("no_auto", "auto"),
    ("non_blocking", "blocking"),
    ("satisfy", "falsify"),
    ("no_user_axioms", "user_axioms"),
@@ -126,31 +133,22 @@
   | NONE => (name, value)
 
 structure TheoryData = TheoryDataFun(
-  type T = {params: raw_param list, registered_auto: bool}
-  val empty = {params = rev default_default_params, registered_auto = false}
+  type T = {params: raw_param list}
+  val empty = {params = rev default_default_params}
   val copy = I
   val extend = I
-  fun merge _ ({params = ps1, registered_auto = a1},
-               {params = ps2, registered_auto = a2}) =
-    {params = AList.merge (op =) (op =) (ps1, ps2),
-     registered_auto = a1 orelse a2})
+  fun merge _ ({params = ps1}, {params = ps2}) =
+    {params = AList.merge (op =) (op =) (ps1, ps2)})
 
 (* raw_param -> theory -> theory *)
 fun set_default_raw_param param thy =
-  let val {params, registered_auto} = TheoryData.get thy in
+  let val {params} = TheoryData.get thy in
     TheoryData.put
-      {params = AList.update (op =) (unnegate_raw_param param) params,
-       registered_auto = registered_auto} thy
+        {params = AList.update (op =) (unnegate_raw_param param) params} thy
   end
 (* theory -> raw_param list *)
 val default_raw_params = #params o TheoryData.get
 
-(* theory -> theory *)
-fun set_registered_auto thy =
-  TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
-(* theory -> bool *)
-val is_registered_auto = #registered_auto o TheoryData.get
-
 (* string -> bool *)
 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
 
@@ -313,8 +311,7 @@
     val uncurry = lookup_bool "uncurry"
     val fast_descrs = lookup_bool "fast_descrs"
     val peephole_optim = lookup_bool "peephole_optim"
-    val timeout = if auto then lookup_time "auto_timeout"
-                  else lookup_time "timeout"
+    val timeout = if auto then NONE else lookup_time "timeout"
     val tac_timeout = lookup_time "tac_timeout"
     val sym_break = Int.max (0, lookup_int "sym_break")
     val sharing_depth = Int.max (1, lookup_int "sharing_depth")
@@ -326,8 +323,8 @@
     val show_consts = show_all orelse lookup_bool "show_consts"
     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
     val evals = lookup_term_list "eval"
-    val max_potential = if auto then 0
-                        else Int.max (0, lookup_int "max_potential")
+    val max_potential =
+      if auto then 0 else Int.max (0, lookup_int "max_potential")
     val max_genuine = Int.max (0, lookup_int "max_genuine")
     val check_potential = lookup_bool "check_potential"
     val check_genuine = lookup_bool "check_genuine"
@@ -412,79 +409,58 @@
        | Refute.REFUTE (loc, details) =>
          error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
 
-(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
+(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
 fun pick_nits override_params auto subgoal state =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val thm = snd (snd (Proof.get_goal state))
+    val thm = state |> Proof.get_goal |> snd |> snd
     val _ = List.app check_raw_param override_params
     val params as {blocking, debug, ...} =
       extract_params ctxt auto (default_raw_params thy) override_params
-    (* unit -> Proof.state *)
+    (* unit -> bool * Proof.state *)
     fun go () =
-      (if auto then perhaps o try
-       else if debug then fn f => fn x => f x
-       else handle_exceptions ctxt)
-      (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
-      state
+      (false, state)
+      |> (if auto then perhaps o try
+          else if debug then fn f => fn x => f x
+          else handle_exceptions ctxt)
+         (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
+                           |>> equal "genuine")
   in
-    if auto orelse blocking then
-      go ()
-    else
-      (SimpleThread.fork true (fn () => (go (); ()));
-       state)
+    if auto orelse blocking then go ()
+    else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
   end
 
 (* (TableFun().key * string list) list option * int option
    -> Toplevel.transition -> Toplevel.transition *)
 fun nitpick_trans (opt_params, opt_subgoal) =
   Toplevel.keep (K ()
-      o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
+      o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
       o Toplevel.proof_of)
 
 (* raw_param -> string *)
 fun string_for_raw_param (name, value) =
   name ^ " = " ^ stringify_raw_param_value value
 
-(* bool -> Proof.state -> Proof.state *)
-fun pick_nits_auto interactive state =
-  let val thy = Proof.theory_of state in
-    ((interactive andalso not (!Toplevel.quiet)
-      andalso the (general_lookup_bool false (default_raw_params thy)
-                  (SOME false) "auto"))
-     ? pick_nits [] true 0) state
-  end
-
-(* theory -> theory *)
-fun register_auto thy =
-  (not (is_registered_auto thy)
-   ? (set_registered_auto
-      #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
-  thy
-
 (* (TableFun().key * string) list option -> Toplevel.transition
    -> Toplevel.transition *)
 fun nitpick_params_trans opt_params =
   Toplevel.theory
-      (fn thy =>
-          let val thy = fold set_default_raw_param (these opt_params) thy in
-            writeln ("Default parameters for Nitpick:\n" ^
-                     (case rev (default_raw_params thy) of
-                        [] => "none"
-                      | params =>
-                        (map check_raw_param params;
-                         params |> map string_for_raw_param |> sort_strings
-                                |> cat_lines)));
-            register_auto thy
-          end)
+      (fold set_default_raw_param (these opt_params)
+       #> tap (fn thy => 
+                  writeln ("Default parameters for Nitpick:\n" ^
+                           (case rev (default_raw_params thy) of
+                              [] => "none"
+                            | params =>
+                              (map check_raw_param params;
+                               params |> map string_for_raw_param
+                                      |> sort_strings |> cat_lines)))))
 
 (* OuterParse.token list
    -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-fun scan_nitpick_command tokens =
-  (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
-fun scan_nitpick_params_command tokens =
-  scan_params tokens |>> nitpick_params_trans
+val scan_nitpick_command =
+  (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
+val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
 
 val _ = OuterSyntax.improper_command "nitpick"
             "try to find a counterexample for a given subgoal using Kodkod"
@@ -493,4 +469,10 @@
             "set and display the default parameters for Nitpick"
             OuterKeyword.thy_decl scan_nitpick_params_command
 
+(* Proof.state -> bool * Proof.state *)
+fun auto_nitpick state =
+  if not (!auto) then (false, state) else pick_nits [] true 1 state
+
+val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
+
 end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Auto_Counterexample.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -0,0 +1,15 @@
+(*  Title:   Tools/Auto_Counterexample.thy
+    Author:  Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+header {* Counterexample Search Unit *}
+
+theory Auto_Counterexample
+imports Pure
+uses
+  "~~/src/Tools/auto_counterexample.ML"
+begin
+
+end

--- a/src/Tools/Code_Generator.thy	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/Tools/Code_Generator.thy	Wed Oct 28 17:43:43 2009 +0100
@@ -5,7 +5,7 @@
 header {* Loading the code generator modules *}
 
 theory Code_Generator
-imports Pure
+imports Auto_Counterexample
 uses
   "~~/src/Tools/value.ML"
   "~~/src/Tools/quickcheck.ML"
@@ -25,4 +25,4 @@
   #> Nbe.setup
 *}
 
-end
\ No newline at end of file
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_counterexample.ML	Wed Oct 28 17:43:43 2009 +0100
@@ -0,0 +1,59 @@
+(*  Title:      Tools/auto_counterexample.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+signature AUTO_COUNTEREXAMPLE =
+sig
+  val time_limit: int Unsynchronized.ref
+
+  val register_tool :
+    string * (Proof.state -> bool * Proof.state) -> theory -> theory
+end;
+
+structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+struct
+
+(* preferences *)
+
+val time_limit = Unsynchronized.ref 2500
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+    (Preferences.nat_pref time_limit
+      "auto-counterexample-time-limit"
+      "Time limit for automatic counterexample search (in milliseconds).")
+
+
+(* configuration *)
+
+structure Data = TheoryDataFun(
+  type T = (string * (Proof.state -> bool * Proof.state)) list
+  val empty = []
+  val copy = I
+  val extend = I
+  fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2)
+)
+
+val register_tool = Data.map o AList.update (op =)
+
+
+(* automatic testing *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
+  case !time_limit of
+    0 => state
+  | ms =>
+    TimeLimit.timeLimit (Time.fromMilliseconds ms)
+        (fn () =>
+            if interact andalso not (!Toplevel.quiet) then
+              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
+                                         | (false, state) => tool state)
+                   (Data.get (Proof.theory_of state)) (false, state) |> snd
+            else
+              state) ()
+    handle TimeLimit.TimeOut =>
+           (warning "Automatic counterexample search timed out."; state)))
+
+end;

--- a/src/Tools/quickcheck.ML	Wed Oct 28 11:55:48 2009 +0100
+++ b/src/Tools/quickcheck.ML	Wed Oct 28 17:43:43 2009 +0100
@@ -7,10 +7,10 @@
 signature QUICKCHECK =
 sig
   val auto: bool Unsynchronized.ref
-  val auto_time_limit: int Unsynchronized.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
+  val setup: theory -> theory
   val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
 end;
 
@@ -20,20 +20,13 @@
 (* preferences *)
 
 val auto = Unsynchronized.ref false;
-val auto_time_limit = Unsynchronized.ref 2500;
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
   (setmp_CRITICAL 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).");
+      "Whether to run Quickcheck automatically.") ());
 
 
 (* quickcheck configuration -- default parameters, test generators *)
@@ -159,28 +152,26 @@
 
 (* automatic testing *)
 
-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);
-    val Test_Params { size, iterations, default_type } =
-      (snd o Data.get o Proof.theory_of) state;
-    fun test () =
-      let
-        val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
-          (try (test_goal true NONE size iterations default_type [] 1 assms)) state;
-      in
-        case res of
-          NONE => state
-        | SOME NONE => state
-        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
-            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
-      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
-  in
-    if int andalso !auto andalso not (!Toplevel.quiet)
-    then test ()
-    else state
-  end));
+fun auto_quickcheck state =
+  if not (!auto) then
+    (false, state)
+  else
+    let
+      val ctxt = Proof.context_of state;
+      val assms = map term_of (Assumption.all_assms_of ctxt);
+      val Test_Params { size, iterations, default_type } =
+        (snd o Data.get o Proof.theory_of) state;
+      val res =
+        try (test_goal true NONE size iterations default_type [] 1 assms) state;
+    in
+      case res of
+        NONE => (false, state)
+      | SOME NONE => (false, state)
+      | SOME cex => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+          Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
+    end
+
+val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
 
 
 (* Isar commands *)
@@ -251,4 +242,3 @@
 
 
 val auto_quickcheck = Quickcheck.auto;
-val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;