src/Pure/ProofGeneral/preferences.ML

--- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -6,6 +6,10 @@
 
 signature PREFERENCES =
 sig
+  val category_display: string
+  val category_advanced_display: string
+  val category_tracing: string
+  val category_proof: string
   type preference =
    {name: string,
     descr: string,
@@ -29,6 +33,14 @@
 structure Preferences: PREFERENCES =
 struct
 
+(* categories *)
+
+val category_display = "Display";
+val category_advanced_display = "Advanced Display";
+val category_tracing = "Tracing";
+val category_proof = "Proof"
+
+
 (* preferences and preference tables *)
 
 type preference =
@@ -66,11 +78,11 @@
 
 (* preferences of Pure *)
 
-val proof_pref =
+val proof_pref = setmp Proofterm.proofs 1 (fn () =>
   let
     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
-  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end;
+  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 
 val thm_depsN = "thm_deps";
 val thm_deps_pref =
@@ -145,24 +157,13 @@
   bool_pref Toplevel.debug
     "debugging"
     "Whether to enable debugging.",
-  bool_pref Quickcheck.auto
-    "auto-quickcheck"
-    "Whether to enable quickcheck automatically.",
-  nat_pref Quickcheck.auto_time_limit
-    "auto-quickcheck-time-limit"
-    "Time limit for automatic quickcheck (in milliseconds).",
-  bool_pref AutoSolve.auto
-    "auto-solve"
-    "Try to solve newly declared lemmas with existing theorems.",
-  nat_pref AutoSolve.auto_time_limit
-    "auto-solve-time-limit"
-    "Time limit for seeking automatic solutions (in milliseconds).",
   thm_deps_pref];
 
 val proof_preferences =
- [bool_pref quick_and_dirty
-    "quick-and-dirty"
-    "Take a few short cuts",
+ [setmp quick_and_dirty true (fn () =>
+    bool_pref quick_and_dirty
+      "quick-and-dirty"
+      "Take a few short cuts") (),
   bool_pref Toplevel.skip_proofs
     "skip-proofs"
     "Skip over proofs (interactive-only)",
@@ -175,10 +176,10 @@
     "Check proofs in parallel"];
 
 val pure_preferences =
- [("Display", display_preferences),
-  ("Advanced Display", advanced_display_preferences),
-  ("Tracing", tracing_preferences),
-  ("Proof", proof_preferences)];
+ [(category_display, display_preferences),
+  (category_advanced_display, advanced_display_preferences),
+  (category_tracing, tracing_preferences),
+  (category_proof, proof_preferences)];
 
 
 (* table of categories and preferences; names must be unique *)