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 ⦄!

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.

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.