# HG changeset patch # User wenzelm # Date 1152620467 -7200 # Node ID 432e914a0e953e5086ddc3c1b4a7e865b2825efe # Parent 99f27df2b6d0bbb30783207b425efa77fb13311f replaced read_radixint by read_intinf; diff -r 99f27df2b6d0 -r 432e914a0e95 src/Pure/library.ML --- a/src/Pure/library.ML Tue Jul 11 14:21:05 2006 +0200 +++ b/src/Pure/library.ML Tue Jul 11 14:21:07 2006 +0200 @@ -163,7 +163,7 @@ val radixstring: int * string * int -> string val string_of_int: int -> string val string_of_indexname: string * int -> string - val read_radixint: int * string list -> int * string list + val read_intinf: int -> string list -> IntInf.int * string list val read_int: string list -> int * string list val oct_char: string -> string @@ -823,19 +823,20 @@ (* read integers *) -fun read_radixint (radix: int, cs) : int * string list = - let val zero = ord"0" - val limit = zero+radix - fun scan (num,[]) = (num,[]) - | scan (num, c::cs) = - if zero <= ord c andalso ord c < limit - then scan(radix*num + ord c - zero, cs) - else (num, c::cs) - in scan(0,cs) end; +fun read_intinf radix cs = + let + val zero = ord "0"; + val limit = zero + radix; + fun scan (num, []) = (num, []) + | scan (num, c :: cs) = + if zero <= ord c andalso ord c < limit then + scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs) + else (num, c :: cs); + in scan (0, cs) end; -fun read_int cs = read_radixint (10, cs); +fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs); -fun oct_char s = chr (#1 (read_radixint (8, explode s))); +fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));