On Sun, 27 Apr 2014, Manuel Eberl wrote:
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.
Please not again this talk about "jEdit". What you mean is
Isabelle/jEdit, which is the default Prover IDE of Isabelle these days.
The difference really matters, because jEdit (the text editor) has many
different ways for abbreviations, completion etc. (You could also add
various input methods of the Java platform, or the operating system.)
In Isabelle/jEdit (the Prover IDE), I had varying default mechanisms for
that over the years. The present one (in Isabelle/5b6f4655e2f2) is quite
advanced, but also quite complex, not to say complicated. In the coming
weeks and months it needs to be polished for the release, but there will
be no further changes of the basic approach, as far as I can forsee.
It is in principle also possible to provide completely different
completion plugins, e.g. if someone wants to imitate the old X-Symbol
behaviour precisely. jEdit is a very flexible text editor, and
Isabelle/jEdit a powerful Prover IDE, which happens to provide certain
defaults out of the box.
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”.
That in isolation is predictable: the completion happens when the result
is unique, and that notion of uniqueness does not change dynamically. That
is the behaviour of Isabelle2013-2, though, since the new semantic
completion introduces a "language context" that sometimes introduces
non-determinism of a different kind, but not the above.
I would prefer a solution that is more suited to my style of typing
“\sigma” and immediately getting “σ”, like in Proof General.
Here you merely need to train your fingers for the exact amount of prefix
required for some symbol. If that does not work, you can leave the
immediate completion off (which is the default). "Like in Proof General"
means just the 4.x line, because that mechanism was quite different until
3.x, when I was still using Proof General myself.
Another problem is that some abbreviations, like “==”, are not
automatically replaced since there are several possibilities.
That is on purpose, to avoid other odd effects. Very ambitious users can
specify their own abbreviations in $ISABELLE_HOME_USER/etc/symbols, and
see themselves how to balance the various possibilities of:
(1) single-character abbreviations, e.g. "%"
(2) unique abbreviations, e.g. "-->"
(3) ambiguous abbrevations, e.g. "=="
Note that "==" is rare in practice anyway, mostly for 'abbreviation'
within the logical environment, which does not happen so often. Unless
you are using old-style definitions with that Pure connective instead of
the normal HOL one.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
