Email Gateway (Aug 22 2022 at 13:00): Email Gateway (Aug 22 2022 at 13:00):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Makarius,
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. For example,
thm list.map_com
completes to "list.map_comp" when I press Ctrl-B. I would find list.map_comp without the
quotes better because they are actually not needed, but I can live with the quotes. The
quotes really get annoying when I use completion for constants inside terms. For example,
when I press Ctrl-B after the underscore in
lemma "monotone ord option.le_ f"
I get
lemma "monotone ord "option.le_fun" f"
and now I have to manually remove the quotes again to avoid parse errors. Is there a way
to avoid the quotes for completion?
Andreas
Email Gateway (Aug 22 2022 at 13:09):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 13:09):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
Thanks for changing the quoting, although I'll have to wait until the next release.
Cheers,
Andreas
Last updated: Apr 19 2024 at 16:20 UTC