[isabelle-dev] Isabelle/jEdit - code completion

Christian Sternagel c.sternagel at gmail.com
Thu May 9 03:34:49 CEST 2013

Dear all,

I think a similar mail was sent a while ago (but I do not remember by 
whom and also was unable to excavate it):

1) In code completion the order of suggestions is sometimes "odd" 
(meaning that a different order would make the usual work-flow 
smoother). E.g., when I start with "find" I usually want 
"find_theorems", but since "find_consts" is first in the list I have to 
type up to "find_t" (or use the arrow keys, which is even worse). Would 
it make sense to prioritize the suggestions (in a way a user can modify 
according to personal preference)?

2) Other code completion suggestions are just too short to make sense at 
all, e.g., when starting with "fo" suggesting "for" seems odd. In my 
opinion, since you need to type at least 2 characters to trigger code 
completion, suggestions that only have 3 letters should not be given, 
since they do not save anything.

3) Another nice thing would be to make code completion context sensitive 
(typically inside quotes you want to get different suggestions than at 
the "top-level").

I'm not saying that those are important issues, just trivial observations.



More information about the isabelle-dev mailing list