Tim Landscheidt <tim@tim-landscheidt.de> writes:
> [ "0x13" is lexed as "0" then "x13" ]
> Is this behaviour really conforming to the standard?
Well, it's pretty much the universal behavior of flex-based lexers,
anyway. A token ends when the next character can no longer sensibly
be added to it.
Possibly the documentation should be tweaked to mention the
number-followed-by-identifier case.
regards, tom lane