[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Makarius wrote:

> On Fri, 27 Jun 2014, Peter Lammich wrote:
>
>>  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.

See again some recent changes-to-changes-to-changes: 0f708666eb7c, 
ff31aad27661.

If the coming Isabelle2014-RC1 does not work smoothly, it should be 
revisited before the final release.


 	Makarius