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 variable instead.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.