# HG changeset patch # User wenzelm # Date 1368560425 -7200 # Node ID 5c179451c445b7f71bfbf3e47e58ed61397ce896 # Parent 5b814dd90f7f05f0b25deb031678c12954d315a5 more elementary pgiptype; diff -r 5b814dd90f7f -r 5c179451c445 src/Pure/ProofGeneral/pgip_types.ML --- 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 diff -r 5b814dd90f7f -r 5c179451c445 src/Pure/ProofGeneral/preferences.ML --- 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 = diff -r 5b814dd90f7f -r 5c179451c445 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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) =>