more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus;

--- 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;
 

--- 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