[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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