[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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