src/Pure/Syntax/parser.ML

   val empty_gram: gram
   val make_gram: Syntax_Ext.xprod list -> Syntax_Ext.xprod list -> gram option -> gram
   val pretty_gram: gram -> Pretty.T list
   datatype tree =
     Markup of Markup.T list * tree list |
-    Node of string * tree list |
+    Node of {nonterm: string, const: string} * tree list |
     Tip of Lexicon.token
   val pretty_tree: tree -> Pretty.T list
   val parse: gram -> string -> Lexicon.token list -> tree list
 end;
 

 
 (* parse tree *)
 
 datatype tree =
   Markup of Markup.T list * tree list |
-  Node of string * tree list |
+  Node of {nonterm: string, const: string} * tree list |
   Tip of Lexicon.token;
 
 datatype tree_op =
   Markup_Push |
   Markup_Pop of Markup.T list |
-  Node_Op of string * tree_op list |
+  Node_Op of {nonterm: int, const: string} * tree_op list |
   Tip_Op of Lexicon.token;
 
 local
   fun drop_markup (Markup_Push :: ts) = drop_markup ts
     | drop_markup (Markup_Pop _ :: ts) = drop_markup ts

 in
   fun tree_ops_ord arg =
     if pointer_eq arg then EQUAL
     else
       (case apply2 drop_markup arg of
-        (Node_Op (s, ts) :: rest, Node_Op (s', ts') :: rest') =>
+        (Node_Op ({const = s, ...}, ts) :: rest, Node_Op ({const = s', ...}, ts') :: rest') =>
           (case fast_string_ord (s, s') of
             EQUAL =>
               (case tree_ops_ord (ts, ts') of
                 EQUAL => tree_ops_ord (rest, rest')
               | ord => ord)

       | ([], _ :: _) => LESS
       | (_ :: _, []) => GREATER
       | _ => raise Match);
 end;
 
-fun make_tree tree_ops =
+fun make_tree names tree_ops =
   let
     fun top [] = []
       | top (xs :: _) = xs;
 
     fun pop [] = []
       | pop (_ :: xs) = xs;
+
+    fun make_name {nonterm = nt, const} =
+      {nonterm = the_name names nt, const = const};
 
     fun make body stack ops =
       (case ops of
         Markup_Push :: rest => make [] (body :: stack) rest
       | Markup_Pop markup :: rest => make (Markup (markup, body) :: top stack) (pop stack) rest
-      | Node_Op (id, ts) :: rest => make (Node (id, make [] [] ts) :: body) stack rest
+      | Node_Op (name, ts) :: rest => make (Node (make_name name, make [] [] ts) :: body) stack rest
       | Tip_Op tok :: rest => make (Tip tok :: body) stack rest
       | [] => if null stack then body else raise Fail "Pending markup blocks");
  in (case make [] [] tree_ops of [t] => SOME t | _ => NONE) end;
 
 fun pretty_tree (Markup (_, ts)) = maps pretty_tree ts
-  | pretty_tree (Node (c, ts)) =
+  | pretty_tree (Node ({const = c, ...}, ts)) =
       [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_tree ts))]
   | pretty_tree (Tip tok) =
       if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
 
 

 fun append_output (Output (m, ss)) (Output (n, ts)) = Output (m + n, ss @ ts);
 
 val output_ord = pointer_eq_ord (fn (Output (m, ss), Output (n, tt)) =>
   (case int_ord (m, n) of EQUAL => tree_ops_ord (ss, tt) | ord => ord));
 
-fun output_tree (Output (_, ts)) = make_tree ts;
+fun output_tree names (Output (_, ts)) = make_tree names ts;
 
 end;
 
 structure Output = Table(type key = output val ord = output_ord);
 

           | Bg markup :: sa => process used ((info, sa, pop_output markup out) :: states) (Si, Sii)
           | En :: sa => process used ((info, sa, push_output out) :: states) (Si, Sii)
           | [] => (*completer operation*)
               let
                 val (A, p, id, j) = info;
-                val out' = if id = "" then out else node_output id out;
+                val out' = node_output {nonterm = A, const = id} out;
                 val (used', Slist) =
                   if j = i then (*lambda production?*)
                     let val (q, used') = update_output (A, (out', p)) used
                     in (used', get_states A q p Si) end
                   else (used, get_states A no_prec p (get j));

         [] => states
       | c :: cs => (process_states gram stateset i c states; produce gram stateset (i + 1) c cs)));
 
 in
 
-fun parse (gram as Gram {tags, ...}) start toks =
+fun parse (gram as Gram {tags, names, ...}) start toks =
   let
     val start_tag =
       (case tags_lookup tags start of
         SOME tag => tag
       | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote start));

     val stateset = Array.array (length input + 1, []);
     val _ = Array.upd stateset 0 [S0];
 
     val result =
       produce gram stateset 0 Lexicon.dummy input
-      |> map_filter (output_tree o #3);
+      |> map_filter (output_tree names o #3);
   in if null result then raise Fail "Inner syntax: no parse trees" else result end;
 
 end;
 
 end;