Re: [isabelle] Completion for long names inserts quotes



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.