Re: [isabelle] Tuning opportunity for auto-completion in Isabelle/Jedit
On Tue, 14 Apr 2015, Bertram Felgenhauer wrote:
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and