[isabelle-dev] Remaining uses of Proof General?

[Manuel Eberl]

Hallo,

I am not, as it were, a user of Proof General anymore; however, I would
like, if I may, to point out one thing that annoys me in jEdit and that
was, in my opinion, better in Proof General: the handling of
abbreviations for Unicode characters.

The current behaviour with “immediate completion” in jEdit is already a
great improvement over having to press “return” or “tab” every time one
wants to use an abbreviation, but one problem that remains is the fact
that jEdit performs the insertion of the character as soon as there is
only one character of that name left, which often leads to somewhat
unpredictable results – for instance, typing “\sigma” results in “σma”.
I would prefer a solution that is more suited to my style of typing
“\sigma” and immediately getting “σ”, like in Proof General. Another
problem is that some abbreviations, like “==”, are not automatically
replaced since there are several possibilities.

In fact, I suppose what I would really like are customisable
instant-replacement abbreviations, like the ones that Proof General
offered. While jEdit does have an “abbreviations” section in its
settings, it would appear they do not work in such a way.

Cheers,
Manuel


On 04/27/14 20:14, Makarius wrote:
> Are there any remaining uses of Proof General, e.g. in the situation
> of current Isabelle/5b6f4655e2f2 ?
>
> This is neither a joke nor a running gag -- I just can't think of
> anything myself after the introduction of the spell checker.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>