[isabelle-dev] NEWS: more informative errors in lazy enumerations
webertj at in.tum.de
Tue Nov 20 15:56:20 CET 2012
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.
More information about the isabelle-dev