# HG changeset patch
# User wenzelm
# Date 1310675431 -7200
# Node ID fad7758421bf07d72a9bd6876ce2dcf07d83ec80
# Parent  7293403dc38b5f20bbe1115386c956d7efb9145b
more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;

diff -r 7293403dc38b -r fad7758421bf src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Jul 13 22:05:55 2011 +0200
+++ b/src/Pure/General/markup.ML	Thu Jul 14 22:30:31 2011 +0200
@@ -136,9 +136,11 @@
 (* integers *)
 
 fun parse_int s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise Fail ("Bad integer: " ^ quote s));
+  let val i = Int.fromString s in
+    if is_none i orelse String.isPrefix "~" s
+    then raise Fail ("Bad integer: " ^ quote s)
+    else the i
+  end;
 
 val print_int = signed_string_of_int;
 
diff -r 7293403dc38b -r fad7758421bf src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Jul 13 22:05:55 2011 +0200
+++ b/src/Pure/General/xml.ML	Thu Jul 14 22:30:31 2011 +0200
@@ -293,9 +293,8 @@
 (* atomic values *)
 
 fun int_atom s =
-  (case Int.fromString s of
-    SOME i => i
-  | NONE => raise XML_ATOM s);
+  Markup.parse_int s
+    handle Fail _ => raise XML_ATOM s;
 
 fun bool_atom "0" = false
   | bool_atom "1" = true