On 28/04/14 04:14, Makarius wrote:
> Are there any remaining uses of Proof General, e.g. in the situation of
current
> Isabelle/5b6f4655e2f2 ?
I'm mostly on Isabelle/jEdit now, but I do delve back into Isabelle/Emacs (is
that the current
terminology for this creature?) every now and then. My reasons are mostly
predictable execution, as
I can control what the prover is up to with explicit stepping forwards and
backwards. I can probably
achieve the same result toggling continuous checking on/off in Isabelle/jEdit,
but haven't invested
the time in modifying my workflow. I've also encountered the problems discussed
in other threads of
the Isabelle/jEdit GUI locking up when some tactic is looping and the JVM heap
being exhausted with
no indication from the UI. However, if PG support disappeared entirely I
wouldn't shed a tear.
Something which used to be a driving factor for me, but no longer is:
Isabelle/Emacs is capable of
running on underpowered machines which do not have enough resources to run
Isabelle/jEdit. This is
not a good reason for maintaining legacy support, but there may be users in
this situation.
On 28/04/14 06:10, Makarius wrote:
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
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
