src/Pure/proof_general.ML
changeset 20364 f7e440f2eb2f
parent 20299 5330f710b960
child 20642 cfe2b0803a51
     1.1 --- a/src/Pure/proof_general.ML	Wed Aug 09 00:12:33 2006 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Aug 09 00:12:35 2006 +0200
     1.3 @@ -503,6 +503,9 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun signed_string_of_int i =
     1.8 +  if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
     1.9 +
    1.10  val pgipint = XML.element "pgipint" [] [];
    1.11  val pgipnat = XML.element "pgipint" [("min", "0")] [];
    1.12  fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
    1.13 @@ -513,7 +516,7 @@
    1.14  in
    1.15  
    1.16  fun int_option r = (pgipint,
    1.17 -  with_default (fn () => string_of_int (! r)),
    1.18 +  with_default (fn () => signed_string_of_int (! r)),
    1.19    (fn s => (case Syntax.read_int s of
    1.20        NONE => error ("int_option: illegal value: " ^ s)
    1.21      | SOME i => r := i)));