[isabelle] Documentation of mixfix annotations

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


  ("⦃_⦄/ _ /(⦃_⦄,/ ⦃_⦄)!") 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

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