[isabelle-dev] White space in theory names
makarius at sketis.net
Fri Jul 4 13:18:18 CEST 2014
On Thu, 12 Jun 2014, Florian Haftmann wrote:
> This is an offspring from
> 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
> 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.
More information about the isabelle-dev