src/Pure/Syntax/parser.ML

 (*  Title:      Pure/Syntax/parser.ML
-    Author:     Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
-
-General context-free parser for the inner syntax of terms, types, etc.
+    Author:     Carsten Clasohm, Sonia Mahjoub
+    Author:     Makarius
+
+General context-free parser for the inner syntax of terms and types.
 *)
 
 signature PARSER =
 sig
   type gram

 
 (** datatype gram **)
 
 (* nonterminals *)
 
-(*production for the NTs are stored in a vector
-  so we can identify NTs by their index*)
+(*production for the NTs are stored in a vector, indexed by the NT tag*)
 type nt = int;
+
+type tags = nt Symtab.table;
+val tags_empty: tags = Symtab.empty;
+fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
+fun tags_lookup (tags: tags) = Symtab.lookup tags;
+fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
+fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
 type nts = Inttab.set;
 val nts_empty: nts = Inttab.empty;
 val nts_merge: nts * nts -> nts = Inttab.merge (K true);
 fun nts_insert nt : nts -> nts = Inttab.insert_set nt;

 fun tokens_find P (tokens: tokens) =
   Tokens.get_first (fn (tok, ()) => if P tok then SOME tok else NONE) tokens;
 fun tokens_add (nt: nt, tokens) = if tokens_is_empty tokens then I else cons (nt, tokens);
 
 
+(* productions *)
+
 datatype symb =
-  Terminal of Lexicon.token
-| Nonterminal of nt * int;  (*(tag, precedence)*)
+  Terminal of Lexicon.token |
+  Nonterminal of nt * int;  (*(tag, prio)*)
 
 type prods = (symb list * string * int) list Tokens.table;  (*start_token ~> [(rhs, name, prio)]*)
 
 val prods_empty: prods = Tokens.empty;
 fun prods_lookup (prods: prods) = Tokens.lookup_list prods;
 fun prods_update entry : prods -> prods = Tokens.update entry;
 fun prods_content (prods: prods) = distinct (op =) (maps #2 (Tokens.dest prods));
 
-type nt_gram =
-  ((nts * tokens) * prods);
-  (*(([dependent_nts], [start_tokens]), prods)*)
-  (*depent_nts is a list of all NTs whose lookahead depends on this NT's lookahead*)
+type nt_gram = (nts * tokens) * prods; (*dependent_nts, start_tokens, prods*)
+  (*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*)
 
 val nt_gram_empty: nt_gram = ((nts_empty, tokens_empty), prods_empty);
-
-type tags = nt Symtab.table;
-val tags_empty: tags = Symtab.empty;
-fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
-fun tags_lookup (tags: tags) = Symtab.lookup tags;
-fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
-fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
 type chains = unit Int_Graph.T;
 fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains;
 fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains;
 fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains;

             (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const)));
   in maps pretty_prod (tags_content tags) end;
 
 
 
-(** Operations on gramars **)
+(** operations on grammars **)
 
 val empty_gram =
   Gram
    {nt_count = 0,
     prod_count = 0,