support for real valued preferences;

--- a/NEWS	Sat Oct 30 16:33:58 2010 +0200
+++ b/NEWS	Sat Oct 30 21:08:20 2010 +0200
@@ -60,6 +60,8 @@
 floating-point notation that coincides with the inner syntax for
 float_token.
 
+* Support for real valued preferences (with approximative PGIP type).
+
 * Interpretation command 'interpret' accepts a list of equations like
 'interpretation' does.
 

--- a/src/Pure/ProofGeneral/pgip_types.ML	Sat Oct 30 16:33:58 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Sat Oct 30 21:08:20 2010 +0200
@@ -22,8 +22,9 @@
 
     (* Types and values (used for preferences and dialogs) *)
 
-    datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
-                      | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
+    datatype pgiptype =
+        Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat | Pgipreal
+      | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
 
     and pgipdtype = Pgipdtype of string option * pgiptype  (* type with opt. description *)
 
@@ -70,7 +71,9 @@
     val read_pgipint       : (int option * int option) -> string -> int (* raises PGIP *)
     val read_pgipnat       : string -> int                              (* raises PGIP *)
     val read_pgipbool      : string -> bool                             (* raises PGIP *)
+    val read_pgipreal      : string -> real                             (* raises PGIP *)
     val read_pgipstring    : string -> string                           (* raises PGIP *)
+    val real_to_pgstring   : real -> string
     val int_to_pgstring    : int -> string
     val bool_to_pgstring   : bool -> string
     val string_to_pgstring : string -> string
@@ -203,6 +206,11 @@
                    else raise PGIP ("Invalid natural number: " ^ quote s)
        | NONE => raise PGIP ("Invalid natural number: " ^ quote s))
 
+fun read_pgipreal s =
+    (case Real.fromString s of
+         SOME x => x
+       | NONE => raise PGIP ("Invalid floating-point number: " ^ quote s))
+
 (* NB: we can maybe do without xml decode/encode here. *)
 fun read_pgipstring s =  (* non-empty strings, XML escapes decoded *)
     (case XML.parse_string s of
@@ -212,6 +220,8 @@
 
 val int_to_pgstring = signed_string_of_int
 
+val real_to_pgstring = signed_string_of_real
+
 fun string_to_pgstring s = XML.text s
 
 fun bool_to_pgstring b = if b then "true" else "false"
@@ -238,6 +248,7 @@
        | Pgipbool                            (* booleans: "true" or "false" *)
        | Pgipint of int option * int option  (* ranged integers, should be XSD canonical *)
        | Pgipnat                             (* naturals: non-negative integers (convenience) *)
+       | Pgipreal                            (* floating-point numbers *)
        | Pgipstring                          (* non-empty strings *)
        | Pgipconst of string                 (* singleton type *)
        | Pgipchoice of pgipdtype list        (* union type *)
@@ -246,8 +257,9 @@
 
 and pgipdtype = Pgipdtype of string option * pgiptype
 
-datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int 
-                  | Pgvalstring of string | Pgvalconst of string
+datatype pgipuval =
+    Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int | Pgvalreal of real
+  | Pgvalstring of string | Pgvalconst of string
 
 type pgipval = pgiptype * pgipuval      (* type-safe values *)
 
@@ -260,6 +272,7 @@
                     | Pgipbool => "pgipbool"
                     | Pgipint _ => "pgipint"
                     | Pgipnat => "pgipint"
+                    | Pgipreal => "pgipint"  (* FIXME sic? *)
                     | Pgipstring => "pgipstring"
                     | Pgipconst _ => "pgipconst"
                     | Pgipchoice _ => "pgipchoice"
@@ -291,6 +304,7 @@
   | read_pguval Pgipbool s = Pgvalbool (read_pgipbool s)
   | read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s)
   | read_pguval Pgipnat s = Pgvalnat (read_pgipnat s)
+  | read_pguval Pgipreal s = Pgvalreal (read_pgipreal s)
   | read_pguval (Pgipconst c) s = 
     if c=s then Pgvalconst c 
     else raise PGIP ("Given string: "^quote s^" doesn't match expected string: "^quote c)
@@ -315,6 +329,7 @@
   | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
   | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
   | pgval_to_string (_, Pgvalint i) = int_to_pgstring i
+  | pgval_to_string (_, Pgvalreal x) = real_to_pgstring x
   | pgval_to_string (_, Pgvalconst c) = string_to_pgstring c
   | pgval_to_string (_, Pgvalstring s) = string_to_pgstring s
 

--- 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));