On Thu, 12 Jun 2014, Florian Haftmann wrote:
This is an offspring from
http://fa.isabelle.narkive.com/QI1dxXvo/isabelle-quotient-type-command-fails
I do not recommend white space in theory names: over the years proper
naming conventions have been increasingly enforced for logical entities
like variable names etc. The issue with theory names maybe just escaped
attention due to its almost extralogical nature.
Allowing white space would be definitely a move in the wrong direction.
Theory names were indeed quite informal some decades ago, but have slowly
gained a more formal and disciplined status, like any other logical entity
with a canonical name space.
The transition towards properly qualified and authentic theory names is
not yet complete, but this spring I got *almost* there. (The attempt was
defeated by various technical side-conditions imposed by the still
existing Isar TTY loop, as well as some unexpected problems with the
HOL-Light importer.)
the fact that the quotient package would cut a name at white space
borders nevertheless seems strange to me and would deserve an inspection.
This is due to "slightly odd bundle trickery" as I called it in my change
745f568837f1, which also removes a deadly "handle _ =>". Note that I was
cleaning up and robustifying other system interfaces in the usual way and
passed-by accidentally (see also 8bedca4bd5a3).
The fragility exposed on this thread is caused by taking an internal long
name, and scanning that again as outer token. This works under the
assumption that names are (qualified) identifiers, which is almost always
the case these days. The qualification prevents overlap with Isar
keywords, unless people define very odd keywords themselves that look like
long identifiers. An alternative is to produce quotes around the name,
before parsing it again.
It is up to Ondřej if he wants to make this yet more robust -- there are
more than 2 weeks left before the Isabelle2014-RC1 repository fork.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
