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:
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
An immediate change to avoid quotes for qualified names is here
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and