At the time I was also wondering whether to allow `sections', eg "(+ 1)" or (1 +)" but did not want to overdo it. It sounds like that at least with your parser imporvements it might be ok?
Tobias On 31/01/2018 22:02, Makarius wrote:
On 10/01/18 20:17, Tobias Nipkow wrote:* The "op <infix-op>" syntax for infix operators has been replaced by "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. In revision eab6ce8368faThat change actually had significant performance impact on some AFP sessions, see http://isabelle.in.tum.de/devel/build_status/AFP around 11-Jan-2018, e.g. HOL-ODE-Numerics, Psi_Calculi, Lorenz_Approximation, Encodability_Process_Calculi. Presumably, the reason for that is the grammar lookahead management with infix operators that require extra space, e.g. '(' '*' ')'. In contrast '(+)' is a distinctive token that does not interfere with other productions. I have already spent a few days reworking the grammar management, see various changes leading up to Isabelle/5f86e2a9c59c. So the AFP performance charts are already converging back to normal, and some sessions are now faster than before. (This also shows how important AFP performance measurement is for continued Isabelle development.) We can ultimately get rid of the extra space for (*) when inner comment syntax is discontinued -- after the next release, according to the normal schedule. Makarius
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
