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 eab6ce8368fa
That 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
