src/Pure/Tools/proof_general_pure.ML

--- a/src/Pure/Tools/proof_general_pure.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed May 15 22:30:24 2013 +0200
@@ -9,42 +9,49 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_types_default
     "show-types"
     "Include types in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_sorts_default
     "show-sorts"
     "Include sorts in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Goal_Display.show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
+    NONE
     @{option names_long}
     "long-names"
     "Show fully qualified names in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_brackets_default
     "show-brackets"
     "Show full bracketing in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Goal_Display.show_main_goal_default
     "show-main-goal"
     "Show main goal in proof state display";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Syntax_Trans.eta_contract_default
     "eta-contract"
     "Print terms eta-contracted";
@@ -54,12 +61,14 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    NONE
     @{option goals_limit}
     "goals-limit"
     "Setting for maximum number of subgoals to be printed";
 
 val _ =
   ProofGeneral.preference ProofGeneral.category_advanced_display
+    NONE
     (Markup.print_int o get_print_depth)
     (print_depth o Markup.parse_int)
     ProofGeneral.pgipint
@@ -68,6 +77,7 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    NONE
     @{option show_question_marks}
     "show-question-marks"
     "Show leading question mark of variable name";
@@ -77,36 +87,42 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Raw_Simplifier.simp_trace_default
     "trace-simplifier"
     "Trace simplification rules";
 
 val _ =
   ProofGeneral.preference_int ProofGeneral.category_tracing
+    NONE
     Raw_Simplifier.simp_trace_depth_limit_default
     "trace-simplifier-depth"
     "Trace simplifier depth limit";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Pattern.trace_unify_fail
     "trace-unification"
     "Output error diagnostics during unification";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Toplevel.timing
     "global-timing"
     "Whether to enable timing in Isabelle";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Toplevel.debug
     "debugging"
     "Whether to enable debugging";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     ProofGeneral.thm_deps
     "theorem-dependencies"
     "Track theorem dependencies within Proof General";
@@ -115,36 +131,38 @@
 (* proof *)
 
 val _ =
-  Unsynchronized.setmp quick_and_dirty true (fn () =>
-    ProofGeneral.preference_bool ProofGeneral.category_proof
-      quick_and_dirty
-      "quick-and-dirty"
-      "Take a few short cuts") ();
+  ProofGeneral.preference_bool ProofGeneral.category_proof
+    (SOME "true")
+    quick_and_dirty
+    "quick-and-dirty"
+    "Take a few short cuts";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_proof
+    NONE
     Goal.skip_proofs
     "skip-proofs"
     "Skip over proofs";
 
 val _ =
-  Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
-    ProofGeneral.preference ProofGeneral.category_proof
-      (Markup.print_bool o Proofterm.proofs_enabled)
-      (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
-      ProofGeneral.pgipbool
-      "full-proofs"
-      "Record full proof objects internally") ();
+  ProofGeneral.preference ProofGeneral.category_proof
+    NONE
+    (Markup.print_bool o Proofterm.proofs_enabled)
+    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
+    ProofGeneral.pgipbool
+    "full-proofs"
+    "Record full proof objects internally";
 
 val _ =
-  Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
-    ProofGeneral.preference_int ProofGeneral.category_proof
-      Multithreading.max_threads
-      "max-threads"
-      "Maximum number of threads") ();
+  ProofGeneral.preference_int ProofGeneral.category_proof
+    NONE
+    Multithreading.max_threads
+    "max-threads"
+    "Maximum number of threads";
 
 val _ =
   ProofGeneral.preference ProofGeneral.category_proof
+    NONE
     (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
     (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
     ProofGeneral.pgipbool