Re: [isabelle] Documentation of mixfix annotations
On Mon, 3 Jun 2013, Lars Noschinski wrote:
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 ⦄!
("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄)!") 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and