# HG changeset patch
# User wenzelm
# Date 1152620468 -7200
# Node ID 7058714024b38242560e491d710fc000daf5dcdf
# Parent  432e914a0e953e5086ddc3c1b4a7e865b2825efe
uniform treatment of num/xnum;
read_xnum: proper handling of bin/hex;

diff -r 432e914a0e95 -r 7058714024b3 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Jul 11 14:21:07 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jul 11 14:21:08 2006 +0200
@@ -264,14 +264,14 @@
       if xids then $$ "_" ^^ scan_id || scan_id
       else scan_id;
 
+    val scan_num = scan_hex || scan_bin || scan_int;
+
     val scan_val =
       scan_tvar >> pair TVarSy ||
       scan_var >> pair VarSy ||
       scan_tid >> pair TFreeSy ||
-      scan_hex >> pair NumSy ||
-      scan_bin >> pair NumSy ||
-      scan_int >> pair NumSy ||
-      $$ "#" ^^ scan_int >> pair XNumSy ||
+      scan_num >> pair NumSy ||
+      $$ "#" ^^ scan_num >> pair XNumSy ||
       scan_longid >> pair LongIdentSy ||
       scan_xid >> pair IdentSy;
 
@@ -368,32 +368,33 @@
     (Scan.read Symbol.stopper scan_digits1 (Symbol.explode s));
 
 
-(* read_xnum *)
+(* read_xnum: hex/bin/decimal *)
 
 local
 
-fun read_intinf cs : IntInf.int * string list =
-  let
-    val zero = ord "0";
-    val limit = zero + 10;
-    fun scan (num, []) = (num, [])
-      | scan (num, c :: cs) =
-          if zero <= ord c andalso ord c < limit
-          then scan (10 * num + IntInf.fromInt (ord c - zero), cs)
-          else (num, c :: cs)
-  in scan (0, cs) end;
+val ten = ord "0" + 10;
+val a = ord "a";
+val A = ord "A";
+val _ = assert (a > A) "Bad ASCII";
+
+fun remap_hex c =
+  let val x = ord c in
+    if x >= a then chr (x - a + ten)
+    else if x >= A then chr (x - A + ten)
+    else c
+  end;
 
 in
 
 fun read_xnum str =
   let
-    val (sign, digs) =
-      (case Symbol.explode str of
-        "#" :: "-" :: cs => (~1, cs)
-      | "#" :: cs => (1, cs)
-      | "-" :: cs => (~1, cs)
-      | cs => (1, cs));
-  in sign * #1 (read_intinf digs) end;
+    val (sign, radix, digs) =
+      (case Symbol.explode (perhaps (try (unprefix "#")) str) of
+        "0" :: "x" :: cs => (1, 16, map remap_hex cs)
+      | "0" :: "b" :: cs => (1, 2, cs)
+      | "-" :: cs => (~1, 10, cs)
+      | cs => (1, 10, cs));
+  in sign * #1 (Library.read_intinf radix digs) end;
 
 end;