# HG changeset patch
# User wenzelm
# Date 1154550413 -7200
# Node ID 5330f710b9607c7302f9297ed4f6d7d0b4231af8
# Parent  6915973e88f3836a01d0fbdaf2ebc769dcadafbc
prems-limit: int_option;

diff -r 6915973e88f3 -r 5330f710b960 src/Pure/proof_general.ML
--- 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)),