On Fri, 27 Jun 2014, Peter Lammich wrote:
* Auto-Completion does not really work. You have to decide for a
"completion delay". If you choose it too short, some completions will
not appear at all. If you choose it too long, it interrupts your typing
flow when entering special characters.
In PG, there is no context-sensitive completion at all ... the one in
jedit is actually not usable without
tolerating .5sec completion delay on every special character you want
to type)
Moreover, the completion mechanism for entering special characters seems
not to be as mature as the one in PG was: When entering sequences that
should be completed, e.g., \lambda, this only works if there are no
characters behind. All in all, I am typing significantly more to enter
special characters than I did in PG.
This belongs to the long completion thread we've had some weeks ago.
You do need to change your practices of typing. Moreover you do need to
find completion options that work for you. There might be even some kind
of "retro legacy setup" that imitates old PG behaviour to some extent, but
I leave it to others to find this out.
I can only say that I am myself typing less and less in recent years, but
I am biased, since I know many fine-points of how it really works.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
