- new auto-quickcheck flag
authorberghofe
Tue, 28 Aug 2007 18:06:24 +0200
changeset 24454 692dac1e7381
parent 24453 86cf57ddf8f6
child 24455 cd8e14100c00
- new auto-quickcheck flag - repaired and inserted proof_pref again
src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Tue Aug 28 18:04:21 2007 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Tue Aug 28 18:06:24 2007 +0200
@@ -58,7 +58,7 @@
 val proof_pref =
     let
         fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
-        fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
+        fun set s = proofs := (if PgipTypes.read_pgipbool s then 2 else 1)
     in
         mkpref get set PgipTypes.Pgipbool "full-proofs"
                "Record full proof objects internally"
@@ -139,7 +139,10 @@
                "Whether to enable timing in Isabelle.",
      bool_pref Toplevel.debug
                 "debugging"
-                "Whether to enable debugging."]
+                "Whether to enable debugging.",
+     bool_pref Codegen.auto_quickcheck
+                "auto-quickcheck"
+                "Whether to enable quickcheck automatically."]
 
 val proof_preferences =
     [bool_pref quick_and_dirty
@@ -148,6 +151,7 @@
      bool_pref Toplevel.skip_proofs
                "skip-proofs"
                "Skip over proofs (interactive-only)",
+     proof_pref,
      nat_pref Multithreading.max_threads
                "max-threads"
                "Maximum number of threads"]