# HG changeset patch
# User wenzelm
# Date 1368648171 -7200
# Node ID 4b77f444afbb25b35cb8da5229e1a99b7a428983
# Parent  d021c180e7df300c4c7f7f76dfb956f678bbad45
simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);

diff -r d021c180e7df -r 4b77f444afbb src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Wed May 15 21:55:09 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Wed May 15 22:02:51 2013 +0200
@@ -18,8 +18,8 @@
   val pgipint: pgiptype
   val pgipfloat: pgiptype
   val pgipstring: pgiptype
-  val preference_raw: category ->
-    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
+  val preference: 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
@@ -89,17 +89,12 @@
 
 (* 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);
-  in
-    add_preference name
-      {category = category, descr = descr, pgiptype = typ, get = get, set = set, default = get ()}
-  end;
+fun preference category get set typ name descr =
+  add_preference name
+    {category = category, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
 
 fun preference_ref category read write typ r =
-  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;
+  preference 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;
diff -r d021c180e7df -r 4b77f444afbb src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Wed May 15 21:55:09 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed May 15 22:02:51 2013 +0200
@@ -59,7 +59,7 @@
     "Setting for maximum number of subgoals to be printed";
 
 val _ =
-  ProofGeneral.preference_raw ProofGeneral.category_advanced_display
+  ProofGeneral.preference ProofGeneral.category_advanced_display
     (Markup.print_int o get_print_depth)
     (print_depth o Markup.parse_int)
     ProofGeneral.pgipint
@@ -129,7 +129,7 @@
 
 val _ =
   Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
-    ProofGeneral.preference_raw ProofGeneral.category_proof
+    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
@@ -144,7 +144,7 @@
       "Maximum number of threads") ();
 
 val _ =
-  ProofGeneral.preference_raw ProofGeneral.category_proof
+  ProofGeneral.preference 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