[isabelle-dev] White space in theory names

[Makarius]

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