Email Gateway (Aug 19 2022 at 11:16): Email Gateway (Aug 19 2022 at 11:16):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I was confused to find that the grammar specified by a mixfix annotation
seems to depend on the pretty printing annotations:
("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄!)") parses only ⦃ P ⦄ f ⦃ Q ⦄, ⦃ A ⦄!
while
("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄)!") parses also ⦃ P ⦄ f ⦃ Q ⦄, ⦃ A ⦄ !
I.e., if the ! is inside the pretty printing block specified by (),
there must not be a space before the !. If it is outside, it may be
preceded by a space.
This kind of makes sense (if you don't allow a space after a pretty
printing block you cannot insert a break) but this behaviour contradicts
the reference manual, which explicitly states right before the syntax of
pretty printing blocks (p.149):
This and the following specifications do not affect parsing at all.
-- Lars
Email Gateway (Aug 19 2022 at 11:19):From: Makarius <makarius@sketis.net>
It affects the collection of literal tokens that are determined by that
grammar production. The above is one of the standard traps about
tokenization, and I reckon that it is explained somewhere in our massive
amounts of manuals.
The usual way to specify separate tokens without additional white space
when printed is to use an empty pretty-printing block "()" in between.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC