# HG changeset patch
# User berghofe
# Date 1188317184 -7200
# Node ID 692dac1e73819d58aaf313228500e31fb7caeb75
# Parent  86cf57ddf8f67ac9ab6baf6319ce1a5d72270579
- new auto-quickcheck flag
- repaired and inserted proof_pref again

diff -r 86cf57ddf8f6 -r 692dac1e7381 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"]