# HG changeset patch
# User wenzelm
# Date 1165879509 -3600
# Node ID 8314ebb5364da7c2a7bbce3f8476b0f7db43485a
# Parent  ec264b9daf94ea25cf7a8a2e186e7cab68855bf0
read_xnum: return leading_zeros, radix;

diff -r ec264b9daf94 -r 8314ebb5364d src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Dec 12 00:25:05 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Dec 12 00:25:09 2006 +0100
@@ -31,7 +31,7 @@
   val var: indexname -> term
   val read_nat: string -> int option
   val read_int: string -> int option
-  val read_xnum: string -> IntInf.int
+  val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int}
   val read_idents: string -> string list
   val fixedN: string
   val constN: string
@@ -397,6 +397,10 @@
     else c
   end;
 
+fun leading_zeros ["0"] = 0
+  | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
+  | leading_zeros _ = 0;
+
 in
 
 fun read_xnum str =
@@ -407,7 +411,8 @@
       | "0" :: "b" :: cs => (1, 2, cs)
       | "-" :: cs => (~1, 10, cs)
       | cs => (1, 10, cs));
-  in sign * #1 (Library.read_intinf radix digs) end;
+    val value = sign * #1 (Library.read_intinf radix digs);
+  in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
 
 end;
 
diff -r ec264b9daf94 -r 8314ebb5364d src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Tue Dec 12 00:25:05 2006 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Tue Dec 12 00:25:09 2006 +0100
@@ -92,7 +92,7 @@
 (* translation of integer constant tokens to and from binary *)
 
 fun int_tr (*"_Int"*) [t as Free (str, _)] =
-      Syntax.const "integ_of" $ mk_bin (Syntax.read_xnum str)
+      Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
   | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
 
 fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)