# HG changeset patch # User wenzelm # Date 1368558169 -7200 # Node ID 5b814dd90f7f05f0b25deb031678c12954d315a5 # Parent cc66addbba6d562acbad8769cf7e8044bcf3b9a9 prefer Markup.parse/print operations -- slight change of exception behaviour; removed obsolete PGIP material; diff -r cc66addbba6d -r 5b814dd90f7f src/Pure/ProofGeneral/pgip_types.ML --- 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) diff -r cc66addbba6d -r 5b814dd90f7f src/Pure/ProofGeneral/preferences.ML --- 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;