# HG changeset patch
# User wenzelm
# Date 1368642166 -7200
# Node ID 0b1183012a3c20c018c5e4ab444e69c96d9d1441
# Parent  9402221f77ddba2e295bb21f615e854c5530f7c9
maintain ProofGeneral preferences within ProofGeneral module;
initialize Isabelle/Pure preferences within normal user space (with antiquotations);
tuned;

diff -r 9402221f77dd -r 0b1183012a3c src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed May 15 20:22:46 2013 +0200
@@ -36,8 +36,8 @@
 val auto_try_max_scopes = 6
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-      (Preferences.bool_pref auto "auto-nitpick" "Run Nitpick automatically.")
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    auto "auto-nitpick" "Run Nitpick automatically"
 
 type raw_param = string * string list
 
diff -r 9402221f77dd -r 0b1183012a3c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 20:22:46 2013 +0200
@@ -45,9 +45,8 @@
 val auto = Unsynchronized.ref false
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-      (Preferences.bool_pref auto "auto-sledgehammer"
-           "Run Sledgehammer automatically.")
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    auto "auto-sledgehammer" "Run Sledgehammer automatically"
 
 (** Sledgehammer commands **)
 
@@ -66,16 +65,16 @@
 val timeout = Unsynchronized.ref 30
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_proof
-      (Preferences.string_pref provers
-          "Sledgehammer: Provers"
-          "Default automatic provers (separated by whitespace)")
+  ProofGeneral.preference_string ProofGeneral.category_proof
+    provers
+    "Sledgehammer: Provers"
+    "Default automatic provers (separated by whitespace)"
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_proof
-      (Preferences.int_pref timeout
-          "Sledgehammer: Time Limit"
-          "ATPs will be interrupted after this time (in seconds)")
+  ProofGeneral.preference_int ProofGeneral.category_proof
+    timeout
+    "Sledgehammer: Time Limit"
+    "ATPs will be interrupted after this time (in seconds)"
 
 type raw_param = string * string list
 
diff -r 9402221f77dd -r 0b1183012a3c src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/HOL/Tools/try0.ML	Wed May 15 20:22:46 2013 +0200
@@ -27,8 +27,8 @@
 val auto = Unsynchronized.ref false
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-      (Preferences.bool_pref auto "auto-try0" "Try standard proof methods.")
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    auto "auto-try0" "Try standard proof methods"
 
 val default_timeout = seconds 5.0
 
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Wed May 15 17:39:41 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,212 +0,0 @@
-(*  Title:      Pure/ProofGeneral/preferences.ML
-    Author:     David Aspinall and Markus Wenzel
-
-User preferences for Isabelle which are maintained by the interface.
-*)
-
-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,
-    default: string,
-    pgiptype: string,
-    get: unit -> string,
-    set: string -> unit}
-  val options_pref: string -> string -> string -> preference
-  val string_pref: string Unsynchronized.ref -> string -> string -> preference
-  val real_pref: real Unsynchronized.ref -> string -> string -> preference
-  val int_pref: int Unsynchronized.ref -> string -> string -> preference
-  val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
-  type T = (string * preference list) list
-  val thm_depsN: string
-  val pure_preferences: T
-  val add: string -> preference -> T -> T
-end
-
-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 =
- {name: string,
-  descr: string,
-  default: string,
-  pgiptype: string,
-  get: unit -> string,
-  set: string -> unit};
-
-val pgipbool = "pgipbool";
-val pgipint = "pgipint";
-val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
-val pgipstring = "pgipstring";
-
-
-(* options as preferences *)
-
-fun options_pref option_name pgip_name descr : preference =
-  let
-    val typ = Options.default_typ option_name;
-    val pgiptype =
-      if typ = Options.boolT then pgipbool
-      else if typ = Options.intT then pgipint
-      else if typ = Options.realT then pgipfloat
-      else pgipstring;
-  in
-   {name = pgip_name,
-    descr = descr,
-    default = Options.get_default option_name,
-    pgiptype = pgiptype,
-    get = fn () => Options.get_default option_name,
-    set = Options.put_default option_name}
-  end;
-
-
-(* generic preferences *)
-
-fun mkpref raw_get raw_set typ name descr : preference =
-  let
-    fun get () = CRITICAL raw_get;
-    fun set x = CRITICAL (fn () => raw_set x);
-  in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end;
-
-fun generic_pref read write typ r =
-  mkpref (fn () => read (! r)) (fn x => r := write x) typ;
-
-val bool_pref = generic_pref Markup.print_bool Markup.parse_bool pgipbool;
-val int_pref = generic_pref Markup.print_int Markup.parse_int pgipint;
-val real_pref = generic_pref Markup.print_real Markup.parse_real pgipfloat;
-val string_pref = generic_pref I I pgipstring;
-
-
-(* preferences of Pure *)
-
-val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
-  let
-    fun get () = Markup.print_bool (Proofterm.proofs_enabled ());
-    fun set s = Proofterm.proofs := (if Markup.parse_bool s then 2 else 1);
-  in mkpref get set pgipbool "full-proofs" "Record full proof objects internally" end) ();
-
-val parallel_proof_pref =
-  let
-    fun get () = Markup.print_bool (! Goal.parallel_proofs >= 1);
-    fun set s = Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0);
-  in mkpref get set pgipbool "parallel-proofs" "Check proofs in parallel" end;
-
-val thm_depsN = "thm_deps";
-val thm_deps_pref =
-  let
-    fun get () = Markup.print_bool (print_mode_active thm_depsN);
-    fun set s =
-      if Markup.parse_bool s
-      then Unsynchronized.change print_mode (insert (op =) thm_depsN)
-      else Unsynchronized.change print_mode (remove (op =) thm_depsN);
-  in
-    mkpref get set pgipbool "theorem-dependencies"
-      "Track theorem dependencies within Proof General"
-  end;
-
-val print_depth_pref =
-  let
-    val get = Markup.print_int o get_print_depth;
-    val set = print_depth o Markup.parse_int;
-  in mkpref get set pgipint "print-depth" "Setting for the ML print depth" end;
-
-
-val display_preferences =
- [bool_pref Printer.show_types_default
-    "show-types"
-    "Include types in display of Isabelle terms",
-  bool_pref Printer.show_sorts_default
-    "show-sorts"
-    "Include sorts in display of Isabelle terms",
-  bool_pref Goal_Display.show_consts_default
-    "show-consts"
-    "Show types of consts in Isabelle goal display",
-  options_pref "names_long"
-    "long-names"
-    "Show fully qualified names in Isabelle terms",
-  bool_pref Printer.show_brackets_default
-    "show-brackets"
-    "Show full bracketing in Isabelle terms",
-  bool_pref Goal_Display.show_main_goal_default
-    "show-main-goal"
-    "Show main goal in proof state display",
-  bool_pref Syntax_Trans.eta_contract_default
-    "eta-contract"
-    "Print terms eta-contracted"];
-
-val advanced_display_preferences =
- [options_pref "goals_limit"
-    "goals-limit"
-    "Setting for maximum number of subgoals to be printed",
-  print_depth_pref,
-  options_pref "show_question_marks"
-    "show-question-marks"
-    "Show leading question mark of variable name"];
-
-val tracing_preferences =
- [bool_pref Raw_Simplifier.simp_trace_default
-    "trace-simplifier"
-    "Trace simplification rules.",
-  int_pref Raw_Simplifier.simp_trace_depth_limit_default
-    "trace-simplifier-depth"
-    "Trace simplifier depth limit.",
-  bool_pref Pattern.trace_unify_fail
-    "trace-unification"
-    "Output error diagnostics during unification",
-  bool_pref Toplevel.timing
-    "global-timing"
-    "Whether to enable timing in Isabelle.",
-  bool_pref Toplevel.debug
-    "debugging"
-    "Whether to enable debugging.",
-  thm_deps_pref];
-
-val proof_preferences =
- [Unsynchronized.setmp quick_and_dirty true (fn () =>
-    bool_pref quick_and_dirty
-      "quick-and-dirty"
-      "Take a few short cuts") (),
-  bool_pref Goal.skip_proofs
-    "skip-proofs"
-    "Skip over proofs",
-  proof_pref,
-  int_pref Multithreading.max_threads
-    "max-threads"
-    "Maximum number of threads",
-  parallel_proof_pref];
-
-val pure_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 *)
-
-type T = (string * preference list) list;
-
-fun add cname (pref: preference) (tab: T) = tab |> map
-  (fn (cat, prefs) =>
-    if cat <> cname then (cat, prefs)
-    else
-      if exists (fn {name, ...} => name = #name pref) prefs
-      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
-      else (cat, prefs @ [pref]));
-
-end;
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/ProofGeneral/proof_general.ML
--- a/src/Pure/ProofGeneral/proof_general.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general.ML	Wed May 15 20:22:46 2013 +0200
@@ -8,28 +8,127 @@
 
 signature PROOF_GENERAL =
 sig
-  val add_preference: string -> Preferences.preference -> unit
+  type category = string
+  val category_display: category
+  val category_advanced_display: category
+  val category_tracing: category
+  val category_proof: category
+  type pgiptype = string
+  val pgipbool: pgiptype
+  val pgipint: pgiptype
+  val pgipfloat: pgiptype
+  val pgipstring: pgiptype
+  val preference_raw: category ->
+    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
+  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
+  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
+  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
+  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
+  val preference_option: category -> string -> string -> string -> unit
+  structure ThyLoad: sig val add_path: string -> unit end
   val init: unit -> unit
-  structure ThyLoad: sig val add_path: string -> unit end
+  val thm_depsN: string
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
 struct
 
-(* preferences *)
+(** preferences **)
+
+(* type preference *)
 
-val preferences = Unsynchronized.ref Preferences.pure_preferences;
+type category = string;
+val category_display = "Display";
+val category_advanced_display = "Advanced Display";
+val category_tracing = "Tracing";
+val category_proof = "Proof";
 
-fun add_preference cat pref =
-  CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref));
+type pgiptype = string;
+val pgipbool = "pgipbool";
+val pgipint = "pgipint";
+val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
+val pgipstring = "pgipstring";
 
-fun set_preference pref value =
-  (case AList.lookup (op =) (map (fn p => (#name p, p)) (maps snd (! preferences))) pref of
-    SOME {set, ...} => set value
-  | NONE => error ("Unknown prover preference: " ^ quote pref));
+type preference =
+ {name: string,
+  descr: string,
+  default: string,
+  pgiptype: pgiptype,
+  get: unit -> string,
+  set: string -> unit};
 
 
-(* process_pgip: minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
+(* global preferences *)
+
+local
+  val preferences =
+    Synchronized.var "ProofGeneral.preferences"
+      ([(category_display, []),
+        (category_advanced_display, []),
+        (category_tracing, []),
+        (category_proof, [])]: (category * preference list) list);
+in
+
+fun add_preference category (pref: preference) =
+  Synchronized.change preferences (map (fn (cat, prefs) =>
+    if cat <> category then (cat, prefs)
+    else
+      if exists (fn {name, ...} => name = #name pref) prefs
+      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
+      else (cat, prefs @ [pref])));
+
+fun get_preferences () = Synchronized.value preferences;
+
+end;
+
+fun set_preference name value =
+  let val prefs = map (`(#name)) (maps snd (get_preferences ())) in
+    (case AList.lookup (op =) prefs name of
+      SOME {set, ...} => set value
+    | NONE => error ("Unknown prover preference: " ^ quote name))
+  end;
+
+
+(* raw preferences *)
+
+fun preference_raw category raw_get raw_set typ name descr =
+  let
+    fun get () = CRITICAL raw_get;
+    fun set x = CRITICAL (fn () => raw_set x);
+    val pref = {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
+  in add_preference category pref end;
+
+fun preference_ref category read write typ r =
+  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;
+
+fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
+fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
+fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
+fun preference_string category = preference_ref category I I pgipstring;
+
+
+(* system options *)
+
+fun preference_option category option_name pgip_name descr =
+  let
+    val typ = Options.default_typ option_name;
+    val pgiptype =
+      if typ = Options.boolT then pgipbool
+      else if typ = Options.intT then pgipint
+      else if typ = Options.realT then pgipfloat
+      else pgipstring;
+  in
+    add_preference category
+     {name = pgip_name,
+      descr = descr,
+      default = Options.get_default option_name,
+      pgiptype = pgiptype,
+      get = fn () => Options.get_default option_name,
+      set = Options.put_default option_name}
+  end;
+
+
+(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)
 
 local
 
@@ -61,14 +160,14 @@
 
 fun invalid_pgip () = raise Fail "Invalid PGIP packet";
 
-fun haspref ({name, descr, default, pgiptype, ...}: Preferences.preference) =
+fun haspref ({name, descr, default, pgiptype, ...}: preference) =
   XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
     [XML.Elem ((pgiptype, []), [])]);
 
 fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
-      ! preferences |> List.app (fn (category, prefs) =>
-          output_pgip refid refseq
-            [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
+      get_preferences () |> List.app (fn (category, prefs) =>
+        output_pgip refid refseq
+          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
   | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
       let
         val name =
@@ -100,6 +199,8 @@
 end;
 
 
+(** messages **)
+
 (* render markup *)
 
 fun special ch = chr 1 ^ ch;
@@ -142,7 +243,7 @@
 end;
 
 
-(* messages *)
+(* hooks *)
 
 fun message bg en prfx text =
   (case render text of
@@ -177,7 +278,18 @@
   emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
 
 
-(* theory loader actions *)
+
+(** theory loader **)
+
+(* fake old ThyLoad -- with new semantics *)
+
+structure ThyLoad =
+struct
+  val add_path = Thy_Load.set_master_path o Path.explode;
+end;
+
+
+(* actions *)
 
 local
 
@@ -226,7 +338,9 @@
   welcome ());
 
 
-(* theorem dependencies *)
+(** theorem dependencies **)
+
+(* thm_deps *)
 
 local
 
@@ -253,7 +367,9 @@
 end;
 
 
-(* report theorem dependencies *)
+(* report via hook *)
+
+val thm_depsN = "thm_deps";
 
 local
 
@@ -265,7 +381,7 @@
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
-  if print_mode_active Preferences.thm_depsN andalso
+  if print_mode_active thm_depsN andalso
     can Toplevel.theory_of state andalso Toplevel.is_theory state'
   then
     let
@@ -281,7 +397,8 @@
 end;
 
 
-(* additional outer syntax for Isar *)
+
+(** Isar command syntax **)
 
 val _ =
   Outer_Syntax.improper_command
@@ -321,7 +438,8 @@
     (Parse.name >> (fn file => Toplevel.imperative (fn () => inform_file_retracted file)));
 
 
-(* init *)
+
+(** init **)
 
 val proof_general_emacsN = "ProofGeneralEmacs";
 
@@ -344,12 +462,7 @@
    Isar.toplevel_loop TextIO.stdIn
     {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
-
-(* fake old ThyLoad -- with new semantics *)
-
-structure ThyLoad =
-struct
-  val add_path = Thy_Load.set_master_path o Path.explode;
 end;
 
-end;
+
+
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/ProofGeneral/proof_general_pure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pure.ML	Wed May 15 20:22:46 2013 +0200
@@ -0,0 +1,158 @@
+(*  Title:      Pure/ProofGeneral/proof_general_pure.ML
+    Author:     David Aspinall
+    Author:     Makarius
+
+Proof General preferences for Isabelle/Pure.
+*)
+
+(* display *)
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Printer.show_types_default
+    "show-types"
+    "Include types in display of Isabelle terms";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Printer.show_sorts_default
+    "show-sorts"
+    "Include sorts in display of Isabelle terms";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Goal_Display.show_consts_default
+    "show-consts"
+    "Show types of consts in Isabelle goal display";
+
+val _ =
+  ProofGeneral.preference_option ProofGeneral.category_display
+    @{option names_long}
+    "long-names"
+    "Show fully qualified names in Isabelle terms";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Printer.show_brackets_default
+    "show-brackets"
+    "Show full bracketing in Isabelle terms";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Goal_Display.show_main_goal_default
+    "show-main-goal"
+    "Show main goal in proof state display";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_display
+    Syntax_Trans.eta_contract_default
+    "eta-contract"
+    "Print terms eta-contracted";
+
+
+(* advanced display *)
+
+val _ =
+  ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    @{option goals_limit}
+    "goals-limit"
+    "Setting for maximum number of subgoals to be printed";
+
+val _ =
+  ProofGeneral.preference_raw ProofGeneral.category_advanced_display
+    (Markup.print_int o get_print_depth)
+    (print_depth o Markup.parse_int)
+    ProofGeneral.pgipint
+    "print-depth"
+    "Setting for the ML print depth";
+
+val _ =
+  ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    @{option show_question_marks}
+    "show-question-marks"
+    "Show leading question mark of variable name";
+
+
+(* tracing *)
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    Raw_Simplifier.simp_trace_default
+    "trace-simplifier"
+    "Trace simplification rules";
+
+val _ =
+  ProofGeneral.preference_int ProofGeneral.category_tracing
+    Raw_Simplifier.simp_trace_depth_limit_default
+    "trace-simplifier-depth"
+    "Trace simplifier depth limit";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    Pattern.trace_unify_fail
+    "trace-unification"
+    "Output error diagnostics during unification";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    Toplevel.timing
+    "global-timing"
+    "Whether to enable timing in Isabelle";
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    Toplevel.debug
+    "debugging"
+    "Whether to enable debugging";
+
+val _ =
+  ProofGeneral.preference_raw ProofGeneral.category_tracing
+    (fn () => Markup.print_bool (print_mode_active ProofGeneral.thm_depsN))
+    (fn s =>
+      if Markup.parse_bool s
+      then Unsynchronized.change print_mode (insert (op =) ProofGeneral.thm_depsN)
+      else Unsynchronized.change print_mode (remove (op =) ProofGeneral.thm_depsN))
+    ProofGeneral.pgipbool
+    "theorem-dependencies"
+    "Track theorem dependencies within Proof General";
+
+
+(* 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") ();
+
+val _ =
+  ProofGeneral.preference_bool ProofGeneral.category_proof
+    Goal.skip_proofs
+    "skip-proofs"
+    "Skip over proofs";
+
+val _ =
+  Unsynchronized.setmp Proofterm.proofs 0 (fn () =>
+    ProofGeneral.preference_raw 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") ();
+
+val _ =
+  Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
+    ProofGeneral.preference_int ProofGeneral.category_proof
+      Multithreading.max_threads
+      "max-threads"
+      "Maximum number of threads") ();
+
+val _ =
+  ProofGeneral.preference_raw ProofGeneral.category_proof
+    (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
+    (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
+    ProofGeneral.pgipbool
+    "parallel-proofs"
+    "Check proofs in parallel";
+
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed May 15 17:39:41 2013 +0200
+++ b/src/Pure/Pure.thy	Wed May 15 20:22:46 2013 +0200
@@ -98,6 +98,7 @@
 ML_file "Isar/isar_syn.ML"
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
+ML_file "ProofGeneral/proof_general_pure.ML"
 
 
 section {* Further content for the Pure theory *}
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/ROOT
--- a/src/Pure/ROOT	Wed May 15 17:39:41 2013 +0200
+++ b/src/Pure/ROOT	Wed May 15 20:22:46 2013 +0200
@@ -160,7 +160,6 @@
     "Proof/proof_rewrite_rules.ML"
     "Proof/proof_syntax.ML"
     "Proof/reconstruct.ML"
-    "ProofGeneral/preferences.ML"
     "ProofGeneral/proof_general.ML"
     "ROOT.ML"
     "Syntax/ast.ML"
diff -r 9402221f77dd -r 0b1183012a3c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed May 15 20:22:46 2013 +0200
@@ -297,12 +297,6 @@
 
 
 (* configuration for Proof General *)
-
-(use
-  |> Unsynchronized.setmp Proofterm.proofs 0
-  |> Unsynchronized.setmp Multithreading.max_threads 0)
-  "ProofGeneral/preferences.ML";
-
 use "ProofGeneral/proof_general.ML";
 
 
diff -r 9402221f77dd -r 0b1183012a3c src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/Tools/quickcheck.ML	Wed May 15 20:22:46 2013 +0200
@@ -97,11 +97,11 @@
 val auto = Unsynchronized.ref false;
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-  (Unsynchronized.setmp auto true (fn () =>
-    Preferences.bool_pref auto
+  Unsynchronized.setmp auto true (fn () =>
+    ProofGeneral.preference_bool ProofGeneral.category_tracing
+      auto
       "auto-quickcheck"
-      "Run Quickcheck automatically.") ());
+      "Run Quickcheck automatically") ()
 
 
 (* quickcheck report *)
diff -r 9402221f77dd -r 0b1183012a3c src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/Tools/solve_direct.ML	Wed May 15 20:22:46 2013 +0200
@@ -37,11 +37,11 @@
 val max_solutions = Unsynchronized.ref 5;
 
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-  (Unsynchronized.setmp auto true (fn () =>
-    Preferences.bool_pref auto
+  Unsynchronized.setmp auto true (fn () =>
+    ProofGeneral.preference_bool ProofGeneral.category_tracing
+      auto
       "auto-solve-direct"
-      ("Run " ^ quote solve_directN ^ " automatically.")) ());
+      ("Run " ^ quote solve_directN ^ " automatically")) ();
 
 
 (* solve_direct command *)
diff -r 9402221f77dd -r 0b1183012a3c src/Tools/try.ML
--- a/src/Tools/try.ML	Wed May 15 17:39:41 2013 +0200
+++ b/src/Tools/try.ML	Wed May 15 20:22:46 2013 +0200
@@ -34,11 +34,11 @@
 
 val auto_time_limit = Unsynchronized.ref 4.0
 
-val auto_try_time_limitN = "auto-try-time-limit"
 val _ =
-  ProofGeneral.add_preference Preferences.category_tracing
-    (Preferences.real_pref auto_time_limit
-      auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
+  ProofGeneral.preference_real ProofGeneral.category_tracing
+    auto_time_limit
+    "auto-try-time-limit"
+    "Time limit for automatically tried tools (in seconds)"
 
 
 (* helpers *)