[isabelle-dev] NEWS: more informative errors in lazy enumerations

Makarius 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 mailing list