--- a/src/Pure/ProofGeneral/pgip_types.ML Tue May 14 21:02:49 2013 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML Tue May 14 21:40:25 2013 +0200
@@ -6,19 +6,10 @@
signature PGIPTYPES =
sig
+ exception PGIP of string
val attr: string -> string -> XML.attributes
val opt_attr: string -> string option -> XML.attributes
val get_attr: XML.attributes -> string -> string (* raises PGIP *)
-
- 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 *)
-
- exception PGIP of string
-
- val pgiptype_to_xml : pgiptype -> XML.tree
end
structure PgipTypes : PGIPTYPES =
@@ -26,8 +17,6 @@
exception PGIP of string
-(** XML utils **)
-
fun get_attr attrs name =
(case Properties.get attrs name of
SOME value => value
@@ -38,77 +27,5 @@
fun opt_attr _ NONE = []
| opt_attr name (SOME value) = attr name value;
-
-(* PGIP datatypes.
-
- This is a reflection of the type structure of PGIP configuration,
- which is meant for setting up user dialogs and preference settings.
- These are configured declaratively in XML, using a syntax for types
- and values which is like a (vastly cut down) form of XML Schema
- Datatypes.
-
- The prover needs to interpret the strings representing the typed
- values, at least for the types it expects from the dialogs it
- configures. Here we go further and construct a type-safe
- encapsulation of these values, which would be useful for more
- advanced cases (e.g. generating and processing forms).
-*)
-
-
-datatype pgiptype =
- Pgipnull (* unit type: unique element is empty string *)
- | 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 *)
-
-(* Compared with the PGIP schema, we push descriptions of types inside choices. *)
-
-and pgipdtype = Pgipdtype of string option * pgiptype
-
-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 *)
-
-fun pgipdtype_to_xml (desco,ty) =
- let
- val desc_attr = opt_attr "descr" desco
-
- val elt = case ty of
- Pgipnull => "pgipnull"
- | Pgipbool => "pgipbool"
- | Pgipint _ => "pgipint"
- | Pgipnat => "pgipint"
- | Pgipreal => "pgipint" (*sic!*) (*required for PG 4.0 and 3.7.x*)
- | Pgipstring => "pgipstring"
- | Pgipconst _ => "pgipconst"
- | Pgipchoice _ => "pgipchoice"
-
- 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)
- | Pgipint (SOME min,NONE) => (range_attr "min" min)
- | Pgipint (NONE,SOME max) => (range_attr "max" max)
- | Pgipnat => (range_attr "min" 0)
- | Pgipconst nm => attr "name" nm
- | _ => []
-
- fun destpgipdtype (Pgipdtype x) = x
-
- val typargs = case ty of
- Pgipchoice ds => map destpgipdtype ds
- | _ => []
- in
- XML.Elem ((elt, desc_attr @ attrs), map pgipdtype_to_xml typargs)
- end
-
-val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
-
end
--- a/src/Pure/ProofGeneral/preferences.ML Tue May 14 21:02:49 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Tue May 14 21:40:25 2013 +0200
@@ -14,7 +14,7 @@
{name: string,
descr: string,
default: string,
- pgiptype: PgipTypes.pgiptype,
+ pgiptype: string,
get: unit -> string,
set: string -> unit}
val options_pref: string -> string -> string -> preference
@@ -45,10 +45,15 @@
{name: string,
descr: string,
default: string,
- pgiptype: PgipTypes.pgiptype,
+ pgiptype: string,
get: unit -> string,
set: string -> unit};
+val pgipbool = "pgipbool";
+val pgipint = "pgipint";
+val pgipfloat = "pgipint"; (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
+val pgipstring = "pgipstring";
+
(* options as preferences *)
@@ -56,10 +61,10 @@
let
val typ = Options.default_typ 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;
+ if typ = Options.boolT then pgipbool
+ else if typ = Options.intT then pgipint
+ else if typ = Options.realT then pgipfloat
+ else pgipstring;
in
{name = pgip_name,
descr = descr,
@@ -81,14 +86,10 @@
fun generic_pref read write typ r =
mkpref (fn () => read (! r)) (fn x => r := write x) typ;
-val string_pref = generic_pref I I PgipTypes.Pgipstring;
-
-val real_pref = generic_pref Markup.print_real Markup.parse_real PgipTypes.Pgipreal;
-
-val int_pref =
- generic_pref Markup.print_int Markup.parse_int (PgipTypes.Pgipint (NONE, NONE));
-
-val bool_pref = generic_pref Markup.print_bool Markup.parse_bool PgipTypes.Pgipbool;
+val bool_pref = generic_pref Markup.print_bool Markup.parse_bool pgipbool;
+val int_pref = generic_pref Markup.print_int Markup.parse_int pgipint;
+val real_pref = generic_pref Markup.print_real Markup.parse_real pgipfloat;
+val string_pref = generic_pref I I pgipstring;
(* preferences of Pure *)
@@ -97,13 +98,13 @@
let
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) ();
+ in mkpref get set pgipbool "full-proofs" "Record full proof objects internally" end) ();
val parallel_proof_pref =
let
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;
+ in mkpref get set pgipbool "parallel-proofs" "Check proofs in parallel" end;
val thm_depsN = "thm_deps";
val thm_deps_pref =
@@ -114,7 +115,7 @@
then Unsynchronized.change print_mode (insert (op =) thm_depsN)
else Unsynchronized.change print_mode (remove (op =) thm_depsN);
in
- mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
+ mkpref get set pgipbool "theorem-dependencies"
"Track theorem dependencies within Proof General"
end;
@@ -122,7 +123,7 @@
let
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;
+ in mkpref get set pgipint "print-depth" "Setting for the ML print depth" end;
val display_preferences =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue May 14 21:02:49 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue May 14 21:40:25 2013 +0200
@@ -51,7 +51,7 @@
fun haspref ({name, descr, default, pgiptype, ...}: Preferences.preference) =
XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
- [PgipTypes.pgiptype_to_xml pgiptype]);
+ [XML.Elem ((pgiptype, []), [])]);
fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
! preferences |> List.app (fn (category, prefs) =>