src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Fri Apr 15 18:43:21 1994 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri Apr 22 12:43:53 1994 +0200
@@ -40,7 +40,7 @@
   include SCANNER
   include LEXICON0
   val is_xid: string -> bool
-  val is_tfree: string -> bool
+  val is_tid: string -> bool
   type lexicon
   datatype token =
     Token of string |
@@ -51,13 +51,14 @@
     EndToken
   val id: string
   val var: string
-  val tfree: string
+  val tid: string
   val tvar: string
   val terminals: string list
   val is_terminal: string -> bool
   val str_of_token: token -> string
   val display_token: token -> string
   val matching_tokens: token * token -> bool
+  val token_assoc: (token option * 'a list) list * token -> 'a list
   val valued_token: token -> bool
   val predef_term: string -> token option
   val dest_lexicon: lexicon -> string list
@@ -83,7 +84,7 @@
     "_" :: cs => is_ident cs
   | cs => is_ident cs);
 
-fun is_tfree s =
+fun is_tid s =
   (case explode s of
     "'" :: cs => is_ident cs
   | _ => false);
@@ -118,10 +119,10 @@
 
 val id = "id";
 val var = "var";
-val tfree = "tfree";
+val tid = "tid";
 val tvar = "tvar";
 
-val terminals = [id, var, tfree, tvar];
+val terminals = [id, var, tid, tvar];
 
 fun is_terminal s = s mem terminals;
 
@@ -141,7 +142,7 @@
 fun display_token (Token s) = quote s
   | display_token (IdentSy s) = "id(" ^ s ^ ")"
   | display_token (VarSy s) = "var(" ^ s ^ ")"
-  | display_token (TFreeSy s) = "tfree(" ^ s ^ ")"
+  | display_token (TFreeSy s) = "tid(" ^ s ^ ")"
   | display_token (TVarSy s) = "tvar(" ^ s ^ ")"
   | display_token EndToken = "";
 
@@ -157,6 +158,17 @@
   | matching_tokens _ = false;
 
 
+(* this function is needed in parser.ML but is placed here 
+   for better performance *)
+fun token_assoc (list, key) =
+  let fun assoc [] = []
+        | assoc ((keyi, xi) :: pairs) =
+            if is_none keyi orelse matching_tokens (the keyi, key) then 
+              (assoc pairs) @ xi
+            else assoc pairs;
+  in assoc list end;
+
+
 (* valued_token *)
 
 fun valued_token (Token _) = false
@@ -172,7 +184,7 @@
 fun predef_term name =
   if name = id then Some (IdentSy name)
   else if name = var then Some (VarSy name)
-  else if name = tfree then Some (TFreeSy name)
+  else if name = tid then Some (TFreeSy name)
   else if name = tvar then Some (TVarSy name)
   else None;