# 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"]