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

[Makarius]

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, 
though).

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.


 	Makarius