src/Pure/Syntax/parser.ML

 val branching_level =
   Config.int (Config.declare ("syntax_branching_level", \<^here>) (fn _ => Config.Int 600));
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
-fun prods_for prods chains include_none tk nts =
+fun prods_for (Gram {prods, chains, ...}) include_none tk nts =
   let
     fun token_assoc (list, key) =
       let
         fun assoc [] result = result
           | assoc ((keyi, pi) :: pairs) result =

           let val nt_prods = snd (Vector.sub (prods, nt));
           in get_prods nts (token_assoc (nt_prods, tk) @ result) end;
   in get_prods (connected_with chains nts nts) [] end;
 
 
-fun PROCESSS prods chains Estate i c states =
+fun PROCESSS gram Estate i c states =
   let
-    fun all_prods_for nt = prods_for prods chains true c [nt];
+    fun all_prods_for nt = prods_for gram true c [nt];
 
     fun processS _ [] (Si, Sii) = (Si, Sii)
       | processS used (S :: States) (Si, Sii) =
           (case S of
             (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) =>

                   in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
               end)
   in processS Inttab.empty states ([], []) end;
 
 
-fun produce prods tags chains stateset i indata prev_token =
+fun produce gram stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
         val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
         val pos = Position.here (Lexicon.pos_of_token prev_token);

   | s =>
       (case indata of
         [] => s
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS prods chains stateset i c s;
+            val (si, sii) = PROCESSS gram stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
-          in produce prods tags chains stateset (i + 1) cs c end));
+          in produce gram stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
 
-fun earley prods tags chains startsymbol indata =
+fun earley (gram as Gram {tags, ...}) startsymbol indata =
   let
     val start_tag =
       (case Symtab.lookup tags startsymbol of
         SOME tag => tag
       | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol));
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
     val _ = Array.update (Estate, 0, S0);
   in
-    get_trees (produce prods tags chains Estate 0 indata Lexicon.eof)
+    get_trees (produce gram Estate 0 indata Lexicon.eof)
   end;
 
 
-fun parse (Gram {tags, prods, chains, ...}) start toks =
+fun parse gram start toks =
   let
     val end_pos =
       (case try List.last toks of
         NONE => Position.none
       | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
     val r =
-      (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
+      (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of
         [] => raise Fail "Inner syntax: no parse trees"
       | pts => pts);
   in r end;