--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Jul 12 22:49:20 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Jul 12 23:45:05 2013 +0200
@@ -12,7 +12,6 @@
val nitpickN : string
val nitpick_paramsN : string
- val auto : bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
val setup : theory -> theory
end;
@@ -29,16 +28,14 @@
val nitpickN = "nitpick"
val nitpick_paramsN = "nitpick_params"
-val auto = Unsynchronized.ref false
-
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
its time slot with several other automatic tools. *)
val auto_try_max_scopes = 6
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_nitpick}
"auto-nitpick"
"Run Nitpick automatically"
@@ -402,6 +399,6 @@
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
-val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
+val setup = Try.register_tool (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
end;