src/Pure/Syntax/lexicon.ML
changeset 11697 8dd899efbd35
parent 9326 1625c1f172b3
child 12785 27debaf2112d
     1.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Oct 05 21:42:10 2001 +0200
     1.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Oct 05 21:48:04 2001 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4      TFreeSy of string |
     1.5      TVarSy of string |
     1.6      NumSy of string |
     1.7 +    XNumSy of string |
     1.8      StrSy of string |
     1.9      EndToken
    1.10    val idT: typ
    1.11 @@ -132,6 +133,7 @@
    1.12    TFreeSy of string |
    1.13    TVarSy of string |
    1.14    NumSy of string |
    1.15 +  XNumSy of string |
    1.16    StrSy of string |
    1.17    EndToken;
    1.18  
    1.19 @@ -144,7 +146,7 @@
    1.20  val tidT = Type ("tid", []);
    1.21  val tvarT = Type ("tvar", []);
    1.22  
    1.23 -val terminals = ["id", "longid", "var", "tid", "tvar", "xnum", "xstr"];
    1.24 +val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
    1.25  
    1.26  fun is_terminal s = s mem terminals;
    1.27  
    1.28 @@ -158,6 +160,7 @@
    1.29    | str_of_token (TFreeSy s) = s
    1.30    | str_of_token (TVarSy s) = s
    1.31    | str_of_token (NumSy s) = s
    1.32 +  | str_of_token (XNumSy s) = s
    1.33    | str_of_token (StrSy s) = s
    1.34    | str_of_token EndToken = "EOF";
    1.35  
    1.36 @@ -170,7 +173,8 @@
    1.37    | display_token (VarSy s) = "var(" ^ s ^ ")"
    1.38    | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
    1.39    | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
    1.40 -  | display_token (NumSy s) = "xnum(" ^ s ^ ")"
    1.41 +  | display_token (NumSy s) = "num(" ^ s ^ ")"
    1.42 +  | display_token (XNumSy s) = "xnum(" ^ s ^ ")"
    1.43    | display_token (StrSy s) = "xstr(" ^ s ^ ")"
    1.44    | display_token EndToken = "";
    1.45  
    1.46 @@ -184,6 +188,7 @@
    1.47    | matching_tokens (TFreeSy _, TFreeSy _) = true
    1.48    | matching_tokens (TVarSy _, TVarSy _) = true
    1.49    | matching_tokens (NumSy _, NumSy _) = true
    1.50 +  | matching_tokens (XNumSy _, XNumSy _) = true
    1.51    | matching_tokens (StrSy _, StrSy _) = true
    1.52    | matching_tokens (EndToken, EndToken) = true
    1.53    | matching_tokens _ = false;
    1.54 @@ -210,6 +215,7 @@
    1.55    | valued_token (TFreeSy _) = true
    1.56    | valued_token (TVarSy _) = true
    1.57    | valued_token (NumSy _) = true
    1.58 +  | valued_token (XNumSy _) = true
    1.59    | valued_token (StrSy _) = true
    1.60    | valued_token EndToken = false;
    1.61  
    1.62 @@ -221,7 +227,8 @@
    1.63    | predef_term "var" = Some (VarSy "var")
    1.64    | predef_term "tid" = Some (TFreeSy "tid")
    1.65    | predef_term "tvar" = Some (TVarSy "tvar")
    1.66 -  | predef_term "xnum" = Some (NumSy "xnum")
    1.67 +  | predef_term "num" = Some (NumSy "num")
    1.68 +  | predef_term "xnum" = Some (XNumSy "xnum")
    1.69    | predef_term "xstr" = Some (StrSy "xstr")
    1.70    | predef_term _ = None;
    1.71  
    1.72 @@ -261,7 +268,8 @@
    1.73        scan_tvar >> pair TVarSy ||
    1.74        scan_var >> pair VarSy ||
    1.75        scan_tid >> pair TFreeSy ||
    1.76 -      $$ "#" ^^ scan_int >> pair NumSy ||
    1.77 +      scan_int >> pair NumSy ||
    1.78 +      $$ "#" ^^ scan_int >> pair XNumSy ||
    1.79        scan_longid >> pair LongIdentSy ||
    1.80        scan_xid >> pair IdentSy;
    1.81  
    1.82 @@ -351,7 +359,8 @@
    1.83        (case Symbol.explode str of
    1.84          "#" :: "-" :: cs => (~1, cs)
    1.85        | "#" :: cs => (1, cs)
    1.86 -      | _ => error ("Malformed number token: " ^ quote str));
    1.87 +      | "-" :: cs => (~1, cs)
    1.88 +      | cs => (1, cs));
    1.89    in sign * #1 (Term.read_int digs) end;
    1.90  
    1.91