On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on options one
could invent long / explicit keywords for them (or Parse.literal items).
grep gives 371 occurences of "-:" in IsaFoR's development repository. So
it's not a rare add-on, but an important performance optimization.
If it is only an optimization it is conceptually still "rare". But of
course it is also possible to invent short keywords -- after some
empricial studies about the danger of clashing with common identifiers.
The datatypes manual calls the above "dead" so that is an obvious choice
to try out.
The BNF package has a slight tendency to cryptic shortcuts to conceal it
from outsiders (like category theory in general).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
