# HG changeset patch
# User wenzelm
# Date 1680369338 -7200
# Node ID 3cc55085d490193da9b81c4f5f830108bf66fd8d
# Parent  9273eb5d26724fb43c9f4e3b4ba91d1876d58036
minor performance tuning;

diff -r 9273eb5d2672 -r 3cc55085d490 src/Pure/General/value.ML
--- a/src/Pure/General/value.ML	Sat Apr 01 16:54:43 2023 +0200
+++ b/src/Pure/General/value.ML	Sat Apr 01 19:15:38 2023 +0200
@@ -31,21 +31,39 @@
 
 (* nat and int *)
 
-val zero = ord "0";
-val nine = ord "9";
+local
+
+val c0 = Char.ord #"0";
+val c9 = Char.ord #"9";
+val minus = Char.ord #"-";
+
+in
+
+fun parse_int str =
+  let
+    fun err () = raise Fail ("Bad integer " ^ quote str);
+    fun char i = Char.ord (String.sub (str, i));
+    val n = size str;
 
-fun parse_nat s =
-  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 digits i a =
+      if i = n then a
+      else
+        let val c = char i
+        in if c0 <= c andalso c <= c9 then digits (i + 1) (10 * a + (c - c0)) else err () end;
+  in
+    if n = 0 then err ()
+    else if char 0 <> minus then digits 0 0
+    else if n = 1 then err ()
+    else ~ (digits 1 0)
+  end;
 
-fun parse_int s =
-  (case try (unprefix "-") s of
-    NONE => parse_nat s
-  | SOME s' => ~ (parse_nat s'))
-  handle Fail _ => raise Fail ("Bad integer " ^ quote s);
+fun parse_nat str =
+  let
+    fun err () = raise Fail ("Bad natural number " ^ quote str);
+    val i = parse_int str handle Fail _ => err ();
+  in if i >= 0 then i else err () end;
+
+end;
 
 val print_int = signed_string_of_int;