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

[Tjark Weber]

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.

Anyway, just dreaming.

Best regards,
Tjark