--- a/src/Pure/ProofGeneral/preferences.ML Sat Oct 30 16:33:58 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Sat Oct 30 21:08:20 2010 +0200
@@ -20,6 +20,7 @@
val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
'a Unsynchronized.ref -> 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 nat_pref: int Unsynchronized.ref -> string -> string -> preference
val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
@@ -65,6 +66,9 @@
val string_pref = generic_pref I I PgipTypes.Pgipstring;
+val real_pref =
+ generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal;
+
val int_pref =
generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
(PgipTypes.Pgipint (NONE, NONE));