# HG changeset patch
# User wenzelm
# Date 1155075155 -7200
# Node ID f7e440f2eb2f04603c2ced21d0cea4734ff4e79c
# Parent  f34c5dbe74d5a758a2c75e54b0336778f8ff995c
int_option: signed_string_of_int;

diff -r f34c5dbe74d5 -r f7e440f2eb2f src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Aug 09 00:12:33 2006 +0200
+++ b/src/Pure/proof_general.ML	Wed Aug 09 00:12:35 2006 +0200
@@ -503,6 +503,9 @@
 
 local
 
+fun signed_string_of_int i =
+  if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
+
 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)] [];
@@ -513,7 +516,7 @@
 in
 
 fun int_option r = (pgipint,
-  with_default (fn () => string_of_int (! r)),
+  with_default (fn () => signed_string_of_int (! r)),
   (fn s => (case Syntax.read_int s of
       NONE => error ("int_option: illegal value: " ^ s)
     | SOME i => r := i)));