[isabelle] Documentation of mixfix annotations
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Documentation of mixfix annotations
- From: Lars Noschinski <noschinl at in.tum.de>
- Date: Mon, 03 Jun 2013 11:40:39 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and