[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jul 25 16:19:48 CEST 2014
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,
If the coming Isabelle2014-RC1 does not work smoothly, it should be
revisited before the final release.
More information about the isabelle-dev