# HG changeset patch
# User wenzelm
# Date 1368373894 -7200
# Node ID 45b972dc78882f7470d80ff8fd7cc6ce0fe804b1
# Parent  3278729bfa3897a94f11c13172ac085df96d5660
support for options as preferences;

diff -r 3278729bfa38 -r 45b972dc7888 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sun May 12 17:42:36 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun May 12 17:51:34 2013 +0200
@@ -17,6 +17,7 @@
     pgiptype: PgipTypes.pgiptype,
     get: unit -> string,
     set: string -> unit}
+  val options_pref: string -> string -> string -> preference
   val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
     'a Unsynchronized.ref -> string -> string -> preference
   val string_pref: string Unsynchronized.ref -> string -> string -> preference
@@ -52,15 +53,36 @@
   get: unit -> string,
   set: string -> unit};
 
+
+(* options as preferences *)
+
+fun options_pref option_name pgip_name descr : preference =
+  let
+    val options = Options.default ();
+    val typ = Options.typ options option_name;
+    val pgiptype =
+      if typ = Options.boolT then PgipTypes.Pgipbool
+      else if typ = Options.intT then PgipTypes.Pgipint (NONE, NONE)
+      else if typ = Options.realT then PgipTypes.Pgipreal
+      else PgipTypes.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;
 
-
-(* generic preferences *)
-
 fun generic_pref read write typ r =
   mkpref (fn () => read (! r)) (fn x => r := write x) typ;