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.


	Makarius





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