src/Tools/quickcheck.ML
changeset 52639 df830310e550
parent 52017 bc0238c1f73a
child 52641 c56b6fa636e8
--- a/src/Tools/quickcheck.ML	Fri Jul 12 22:49:20 2013 +0200
+++ b/src/Tools/quickcheck.ML	Fri Jul 12 23:45:05 2013 +0200
@@ -12,7 +12,6 @@
   val unknownN: string
   val setup: theory -> theory
   (*configuration*)
-  val auto: bool Unsynchronized.ref
   val batch_tester : string Config.T
   val size : int Config.T
   val iterations : int Config.T
@@ -94,12 +93,10 @@
 
 (* preferences *)
 
-val auto = Unsynchronized.ref false;
-
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
+  ProofGeneral.preference_option ProofGeneral.category_tracing
     (SOME "true")
-    auto
+    @{option auto_quickcheck}
     "auto-quickcheck"
     "Run Quickcheck automatically";
 
@@ -567,8 +564,7 @@
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN);
 
-val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck));
+val setup = Try.register_tool (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
 
 end;
 
-val auto_quickcheck = Quickcheck.auto;