--- a/src/Pure/proof_general.ML Wed Aug 02 22:26:52 2006 +0200
+++ b/src/Pure/proof_general.ML Wed Aug 02 22:26:53 2006 +0200
@@ -503,6 +503,7 @@
local
+val pgipint = XML.element "pgipint" [] [];
val pgipnat = XML.element "pgipint" [("min", "0")] [];
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
val pgipbool = XML.element "pgipbool" [] [];
@@ -511,6 +512,12 @@
in
+fun int_option r = (pgipint,
+ with_default (fn () => string_of_int (! r)),
+ (fn s => (case Syntax.read_int s of
+ NONE => error ("int_option: illegal value: " ^ s)
+ | SOME i => r := i)));
+
fun nat_option r = (pgipnat,
with_default (fn () => string_of_int (! r)),
(fn s => (case Syntax.read_nat s of
@@ -574,7 +581,7 @@
nat_option goals_limit)),
("prems-limit",
("Setting for maximum number of premises printed",
- nat_option ProofContext.prems_limit)),
+ int_option ProofContext.prems_limit)),
("print-depth",
("Setting for the ML print depth",
print_depth_option)),