Re: [isabelle] Remaining reasons for Proof General


Am Dienstag, den 12.11.2013, 15:54 +0100 schrieb Manuel Eberl:
> Another problem are codes such as "not", which are still not replaced at
> all, since "notation", "note" and so on also exist. I'm afraid I don't
> think I can get used to this.

for not, I use ~<TAB>. Not consistent with the others, but still fast.

In any case I believe that jEdit is an editor capable of suiting most
uses when it comes to abbreviations, navigation etc. It surely takes
time to find out how things work, and even more how to change the
behavior if it does not work as intended, and what fancy plugins are

Ideally most of the issues that we discussed in this thread about
symbols are actually independent from whether we edit Isabelle theories
or love letters (\he gives ♡ ;-)), so that we can use upstream resources
when solving them.
I’m not sure if this is actually the case, though, as I cannot tell
which editing features are provided by jEdit by default, which are
provided by jEdit but instrumented and configured using the Isabelle
plugin, and which are genuine Isabelle plugin features.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.