Re: [isabelle] Completion for long names inserts quotes



Hi Makarius,

Thanks for changing the quoting, although I'll have to wait until the next release.

Cheers,
Andreas

On 14/04/16 11:50, Makarius wrote:
On Thu, 17 Mar 2016, Andreas Lochbihler wrote:

I like to use completion for constant and theorem names. Unfortunately, if the theorem
completes to a long name (i.e., something of the form xxx.yyyy), then completion wraps
this in quotes.

Is there a way to avoid the quotes for completion?

This is a hardwired heuristic here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016/src/Pure/General/completion.scala#l211


Long identifiers are quoted due to a confusion of Token.is_name vs. Token.is_xname. The
test is generally a bit crude, because the syntax context is not observed, e.g. there
could be an undetected conflict with keywords.


An immediate change to avoid quotes for qualified names is here
http://isabelle.in.tum.de/repos/isabelle/rev/d0c1b2dbca5b

Moreover, since the distinction of unqualified "name" vs. potentially qualified "xname"
categories often leads to confusion, I've smashed that in 9f394a16c557 to just one "name"
category. (At some point we might even want to allow qualified names in binding positions,
which requires such a syntax change anyway.)

These changes are for the next release, towards the end of the year 2016.


     Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.