prefer Markup.parse/print operations -- slight change of exception behaviour;
removed obsolete PGIP material;

--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue May 14 20:46:09 2013 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Tue May 14 21:02:49 2013 +0200
@@ -18,18 +18,6 @@
 
   exception PGIP of string
 
-  (* Values as XML strings *)
-  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
-
-  (* PGIP datatypes *)
   val pgiptype_to_xml   : pgiptype -> XML.tree
 end
 
@@ -51,55 +39,6 @@
   | opt_attr name (SOME value) = attr name value;
 
 
-(** Types and values **)
-
-fun read_pgipbool s =
-    (case s of
-         "false" => false
-       | "true" => true
-       | _ => raise PGIP ("Invalid boolean value: " ^ quote s))
-
-local
-    fun int_in_range (NONE,NONE) (_: int) = true
-      | int_in_range (SOME min,NONE) i = min<= i
-      | int_in_range (NONE,SOME max) i = i<=max
-      | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max
-in
-fun read_pgipint range s =
-    (case Int.fromString s of
-         SOME i => if int_in_range range i then i
-                   else raise PGIP ("Out of range integer value: " ^ quote s)
-       | NONE => raise PGIP ("Invalid integer value: " ^ quote s))
-end;
-
-fun read_pgipnat s =
-    (case Int.fromString s of
-         SOME i => if i >= 0 then i
-                   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
-         SOME s => s
-       | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
-    handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)  (* FIXME avoid handle _ *)
-
-val int_to_pgstring = signed_string_of_int
-
-val real_to_pgstring = Markup.print_real;
-
-
-fun string_to_pgstring s = XML.text s
-
-fun bool_to_pgstring b = if b then "true" else "false"
-
-
 (* PGIP datatypes.
 
    This is a reflection of the type structure of PGIP configuration,
@@ -150,7 +89,7 @@
                     | Pgipconst _ => "pgipconst"
                     | Pgipchoice _ => "pgipchoice"
 
-        fun range_attr r v = attr r (int_to_pgstring v)
+        fun range_attr r v = attr r (Markup.print_int v)
 
         val attrs = case ty of
                         Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)

--- a/src/Pure/ProofGeneral/preferences.ML	Tue May 14 20:46:09 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Tue May 14 21:02:49 2013 +0200
@@ -83,37 +83,34 @@
 
 val string_pref = generic_pref I I PgipTypes.Pgipstring;
 
-val real_pref =
-  generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal;
+val real_pref = generic_pref Markup.print_real Markup.parse_real PgipTypes.Pgipreal;
 
 val int_pref =
-  generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
-    (PgipTypes.Pgipint (NONE, NONE));
+  generic_pref Markup.print_int Markup.parse_int (PgipTypes.Pgipint (NONE, NONE));
 
-val bool_pref =
-  generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
+val bool_pref = generic_pref Markup.print_bool Markup.parse_bool PgipTypes.Pgipbool;
 
 
 (* preferences of Pure *)
 
 val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
   let
-    fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
-    fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
+    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 PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 
 val parallel_proof_pref =
   let
-    fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
-    fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
+    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 PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
 
 val thm_depsN = "thm_deps";
 val thm_deps_pref =
   let
-    fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
+    fun get () = Markup.print_bool (print_mode_active thm_depsN);
     fun set s =
-      if PgipTypes.read_pgipbool 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
@@ -123,8 +120,8 @@
 
 val print_depth_pref =
   let
-    fun get () = PgipTypes.int_to_pgstring (get_print_depth ());
-    val set = print_depth o PgipTypes.read_pgipnat;
+    val get = Markup.print_int o get_print_depth;
+    val set = print_depth o Markup.parse_int;
   in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end;