# HG changeset patch
# User wenzelm
# Date 1513450960 -3600
# Node ID e62d72699666c4e70ae433137ce6d9d6148aabea
# Parent  53867014e299f2fe0a6aad80a5fe44dce9387239
more accurate parse_nat/parse_int: avoid corner cases of Int.fromString (e.g. "1.0");

diff -r 53867014e299 -r e62d72699666 src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Sat Dec 16 17:23:00 2017 +0100
+++ b/src/Pure/General/value.ML	Sat Dec 16 20:02:40 2017 +0100
@@ -31,19 +31,21 @@
 
 (* nat and int *)
 
+val zero = ord "0";
+val nine = ord "9";
+
 fun parse_nat s =
-  let val i = Int.fromString s in
-    if is_none i orelse the i < 0
-    then raise Fail ("Bad natural number " ^ quote s)
-    else the i
-  end;
+  fold_string (fn c => fn n =>
+    let val i = ord c in
+      if zero <= i andalso i <= nine then 10 * n + (i - zero)
+      else raise Fail ("Bad natural number " ^ quote s)
+    end) s 0;
 
 fun parse_int 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;
+  (case try (unprefix "-") s of
+    NONE => parse_nat s
+  | SOME s' => ~ (parse_nat s'))
+  handle Fail _ => raise Fail ("Bad integer " ^ quote s);
 
 val print_int = signed_string_of_int;