Email Gateway (Aug 22 2022 at 09:10): Email Gateway (Aug 22 2022 at 09:10):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Hi,
I noticed that when listing completions (in Isabelle/Jedit) for
thm ex or thm ext
(with the cursor after the x and t respectively), the fact "ext"
is not listed. I found this rather surprising.
This happens with both Isabelle 2014 and 2015 RC0, in a trivial
theory file that just imports Main.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 09:10):From: Makarius <makarius@sketis.net>
This is because the completion_limit (default 40) truncates this rather
long list of names with the popular prefix "ex".
Instead of increasing the limit, which would make the dialog harder to
use, the usual way is to provide a longer prefix to complete. Giving
"ext" does not work, though, because it is already complete, and thus
suppressed in the result.
To force a completion nonetheless, you can add an extra underscore: so
"ext_" will offer a completion to "ext" (fact "HOL.ext") as expected, even
though it makes little sense to do this in practice.
Makarius
Email Gateway (Aug 22 2022 at 09:10):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Dear Makarius,
This is because the completion_limit (default 40) truncates this rather long
list of names with the popular prefix "ex".
Thanks, that makes sense.
Instead of increasing the limit, which would make the dialog harder to use,
the usual way is to provide a longer prefix to complete. Giving "ext" does
not work, though, because it is already complete, and thus suppressed in the
result.
Is it possible to disable this suppression of exact matches without having
to append an underscore? I think I would prefer that behavior.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 09:10):From: Makarius <makarius@sketis.net>
Semantic completion was already introduced in Isabelle2014 and did not
change for Isabelle2015. So just formally, it would be a bad idea to
tinker with it now, i.e. "fix it". These heuristics are not so obvious, in
fact there is a bit too much AI in it for my taste, but I did not have
substantially better ideas since then.
The underscore to force a completion in a situation where the system
prefers not to complete by default is very central. Every expert user
should know it. Within the term language it is unavoidable anyway, e.g.
to complete consts and not have some partial input accepted as free
variable instead.
Makarius
Email Gateway (Aug 22 2022 at 09:11):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Dear Makarius,
Right, I was wondering whether a flag for configuring this behavior
exists. But I guess I'll just have to become used to the suppressions.
Cheers,
Bertram
Last updated: Apr 26 2024 at 12:28 UTC