# HG changeset patch
# User wenzelm
# Date 1002311284 -7200
# Node ID 8dd899efbd35bb2149aaeccbccf8e127eecac285
# Parent  233362cfecc7ee54b98ec6101b26a2151caa1c76
added "num" token;

diff -r 233362cfecc7 -r 8dd899efbd35 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Oct 05 21:42:10 2001 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Oct 05 21:48:04 2001 +0200
@@ -46,6 +46,7 @@
     TFreeSy of string |
     TVarSy of string |
     NumSy of string |
+    XNumSy of string |
     StrSy of string |
     EndToken
   val idT: typ
@@ -132,6 +133,7 @@
   TFreeSy of string |
   TVarSy of string |
   NumSy of string |
+  XNumSy of string |
   StrSy of string |
   EndToken;
 
@@ -144,7 +146,7 @@
 val tidT = Type ("tid", []);
 val tvarT = Type ("tvar", []);
 
-val terminals = ["id", "longid", "var", "tid", "tvar", "xnum", "xstr"];
+val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
 
 fun is_terminal s = s mem terminals;
 
@@ -158,6 +160,7 @@
   | str_of_token (TFreeSy s) = s
   | str_of_token (TVarSy s) = s
   | str_of_token (NumSy s) = s
+  | str_of_token (XNumSy s) = s
   | str_of_token (StrSy s) = s
   | str_of_token EndToken = "EOF";
 
@@ -170,7 +173,8 @@
   | display_token (VarSy s) = "var(" ^ s ^ ")"
   | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
   | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
-  | display_token (NumSy s) = "xnum(" ^ s ^ ")"
+  | display_token (NumSy s) = "num(" ^ s ^ ")"
+  | display_token (XNumSy s) = "xnum(" ^ s ^ ")"
   | display_token (StrSy s) = "xstr(" ^ s ^ ")"
   | display_token EndToken = "";
 
@@ -184,6 +188,7 @@
   | matching_tokens (TFreeSy _, TFreeSy _) = true
   | matching_tokens (TVarSy _, TVarSy _) = true
   | matching_tokens (NumSy _, NumSy _) = true
+  | matching_tokens (XNumSy _, XNumSy _) = true
   | matching_tokens (StrSy _, StrSy _) = true
   | matching_tokens (EndToken, EndToken) = true
   | matching_tokens _ = false;
@@ -210,6 +215,7 @@
   | valued_token (TFreeSy _) = true
   | valued_token (TVarSy _) = true
   | valued_token (NumSy _) = true
+  | valued_token (XNumSy _) = true
   | valued_token (StrSy _) = true
   | valued_token EndToken = false;
 
@@ -221,7 +227,8 @@
   | predef_term "var" = Some (VarSy "var")
   | predef_term "tid" = Some (TFreeSy "tid")
   | predef_term "tvar" = Some (TVarSy "tvar")
-  | predef_term "xnum" = Some (NumSy "xnum")
+  | predef_term "num" = Some (NumSy "num")
+  | predef_term "xnum" = Some (XNumSy "xnum")
   | predef_term "xstr" = Some (StrSy "xstr")
   | predef_term _ = None;
 
@@ -261,7 +268,8 @@
       scan_tvar >> pair TVarSy ||
       scan_var >> pair VarSy ||
       scan_tid >> pair TFreeSy ||
-      $$ "#" ^^ scan_int >> pair NumSy ||
+      scan_int >> pair NumSy ||
+      $$ "#" ^^ scan_int >> pair XNumSy ||
       scan_longid >> pair LongIdentSy ||
       scan_xid >> pair IdentSy;
 
@@ -351,7 +359,8 @@
       (case Symbol.explode str of
         "#" :: "-" :: cs => (~1, cs)
       | "#" :: cs => (1, cs)
-      | _ => error ("Malformed number token: " ^ quote str));
+      | "-" :: cs => (~1, cs)
+      | cs => (1, cs));
   in sign * #1 (Term.read_int digs) end;
 
 
diff -r 233362cfecc7 -r 8dd899efbd35 src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Fri Oct 05 21:42:10 2001 +0200
+++ b/src/Pure/Syntax/token_trans.ML	Fri Oct 05 21:48:04 2001 +0200
@@ -51,7 +51,7 @@
 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
 
 val standard_token_classes =
-  ["class", "tfree", "tvar", "free", "bound", "var", "xnum", "xstr"];
+  ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];