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