[isabelle-dev] NEWS: more informative errors in lazy enumerations
makarius at sketis.net
Tue Nov 20 16:05:55 CET 2012
On Tue, 20 Nov 2012, Tjark Weber wrote:
> On Tue, 2012-11-20 at 15:24 +0100, Makarius wrote:
>> I have many more things on my list to improve the completion mechanism,
>> before such a detail would be considered again.
> A huge step forward, in my humble opinion, would be context-sensitive
> completion. For instance, I would ideally like the IDE to figure out
> whether I am typing "le" to obtain "lemma" or "≤".
> If this works well, one could then also consider completion for
> methods, theorem names, logical constants, and whatnot.
Yes, this is one of the things on the list (not for the coming release,
What might happen before the release is a move from Sidekick/completion
subplugin, to the new Completion standalone-plugin from the jEdit guys.
It depends if their release schedule recovers after the summer break -- I
don't see any important activity there since 01-Sep-2012, whicj was the
original plan for jEdit 5.0 to be rolled out.
More information about the isabelle-dev