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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev