Re: terminal @number vs. @user-number

[Wojciech Polak]

On 2007-10-21 at 17:46 -0400, Joel E. Denny wrote:

> Currently, Bison puts a terminal's user number (the one returned by yylex) 
> in its XML "number" attribute.  I think we should rename that to 
> "user-number" and add a "number" attribute for Bison's internal symbol 
> number.  This would be more consistent with nonterminals.
> I'd be happy the write the patch.  Is all this agreeable to you, Wojciech?

Can you write more about the practical goal (and its further usage)
of having two numbers, especially Bison's internal symbol number?
Maybe it's okay to switch, but to have only one kind of number,
thus changing nonterminal, and not terminal?

Regards,
Wojciech