# HG changeset patch
# User wenzelm
# Date 1230056862 -3600
# Node ID 89f76a58a378dbf1efae582626b1aa60ca4596e7
# Parent  ca28610a0e7edc80ea20cc300c667fc3d6d1b8fc
renamed terminal category "float" to "float_token", to avoid name
  space conflicts with actual "float" types in user theories (only
  "float_const" is encountered in practice anyway);
tuned;

diff -r ca28610a0e7e -r 89f76a58a378 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Dec 23 13:20:34 2008 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Dec 23 19:27:42 2008 +0100
@@ -145,8 +145,18 @@
 val tidT = Type ("tid", []);
 val tvarT = Type ("tvar", []);
 
-val terminals =
-  ["id", "longid", "var", "tid", "tvar", "num", "float", "xnum", "xstr"];
+val terminal_kinds =
+ [("id", IdentSy),
+  ("longid", LongIdentSy),
+  ("var", VarSy),
+  ("tid", TFreeSy),
+  ("tvar", TVarSy),
+  ("num", NumSy),
+  ("float_token", FloatSy),
+  ("xnum", XNumSy),
+  ("xstr", StrSy)];
+
+val terminals = map #1 terminal_kinds;
 val is_terminal = member (op =) terminals;
 
 
@@ -186,16 +196,10 @@
 
 (* predef_term *)
 
-fun predef_term "id" = SOME (Token (IdentSy, "id", Position.no_range))
-  | predef_term "longid" = SOME (Token (LongIdentSy, "longid", Position.no_range))
-  | predef_term "var" = SOME (Token (VarSy, "var", Position.no_range))
-  | predef_term "tid" = SOME (Token (TFreeSy, "tid", Position.no_range))
-  | predef_term "tvar" = SOME (Token (TVarSy, "tvar", Position.no_range))
-  | predef_term "num" = SOME (Token (NumSy, "num", Position.no_range))
-  | predef_term "float" = SOME (Token (FloatSy, "float", Position.no_range))
-  | predef_term "xnum" = SOME (Token (XNumSy, "xnum", Position.no_range))
-  | predef_term "xstr" = SOME (Token (StrSy, "xstr", Position.no_range))
-  | predef_term _ = NONE;
+fun predef_term s =
+  (case AList.lookup (op =) terminal_kinds s of
+    SOME sy => SOME (Token (sy, s, Position.no_range))
+  | NONE => NONE);
 
 
 (* xstr tokens *)
@@ -382,21 +386,27 @@
       | "0" :: "b" :: cs => (1, 2, cs)
       | "-" :: cs => (~1, 10, cs)
       | cs => (1, 10, cs));
-    val value = sign * #1 (Library.read_radix_int radix digs);
-  in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
+  in
+   {radix = radix,
+    leading_zeros = leading_zeros digs,
+    value = sign * #1 (Library.read_radix_int radix digs)}
+  end;
 
 end;
 
 fun read_float str =
   let
     val (sign, cs) =
-      (case Symbol.explode str of  "-" :: cs => (~1, cs) | cs => (1, cs));
-    val (intpart,fracpart) =
+      (case Symbol.explode str of
+        "-" :: cs => (~1, cs)
+      | cs => (1, cs));
+    val (intpart, fracpart) =
       (case take_prefix Symbol.is_digit cs of
-        (intpart, "." :: fracpart) => (intpart,fracpart)
-      | _ =>  sys_error "read_float")
-  in {mant = sign * #1 (Library.read_int (intpart@fracpart)),
-      exp = length fracpart}
+        (intpart, "." :: fracpart) => (intpart, fracpart)
+      | _ => raise Fail "read_float");
+  in
+   {mant = sign * #1 (Library.read_int (intpart @ fracpart)),
+    exp = length fracpart}
   end
 
 end;
diff -r ca28610a0e7e -r 89f76a58a378 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Dec 23 13:20:34 2008 +0100
+++ b/src/Pure/pure_thy.ML	Tue Dec 23 19:27:42 2008 +0100
@@ -322,7 +322,7 @@
     ("",            typ "var => logic",                Delimfix "_"),
     ("_DDDOT",      typ "logic",                       Delimfix "..."),
     ("_constify",   typ "num => num_const",            Delimfix "_"),
-    ("_constify",   typ "float => float_const",        Delimfix "_"),
+    ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),