Re: [isabelle] Remaining reasons for Proof General
On Mon, 11 Nov 2013, René Neumann wrote:
Am 11.11.2013 12:34, schrieb Makarius:
People who are still using Proof General should say more explicitly what
are the reasons for it,
I think, I had put it in another mail already, but well:
IIRC, that was for Isabelle2013. So for Isabelle/PIDE 3rd generation.
Now we have Isabelle2013-1 and the 4th generation.
One of the big differences to Proof General is that there are big
differences in each release cycle. You really need to look what is there
- jEdit is SLOW, as in: There is a noticeable lag when moving from one
menu to the other per mouse (rendering also consumes 50% to 100% of one
What is your hardware like? I usually see 20% total time for the JVM and
approx. 400-800% for Isabelle/ML. That is an old 8 core machine from
Java has this odd feature that it sometimes "looks slow", but it actually
Isabelle/jEdit was started in 2008 to make efficient use of current
hardware (2 cores or more).
- Fonts are not antialiased. I found that setting some obscure
environment variable  made it work, but honestly: no AA by default is
Obsolete in Isabelle2013-1 and hardly an issue before, since it was well
documented in the jEdit FAQ how to change such defaults.
- no switching of sessions (at least last time I checked)
Rarely needed, unless you make a convincing point for such a marginal
feature. In Isabelle/jEdit you can load disjoint sessions without
interfering each other.
Proof General legacy support is actually in the way to clean up all that
and make just one way of Isabelle build or Isabelle/jEdit with multiple
- (obsolete: my WM fails to show jEdits dialogs. Just noticed that there
is a patch available for it).
What is your WM? There are many Linux guys who just don't want Java
applications on their particular fork. The solution is to use one of the
well-known standard window managers.
- jEdit is too mouse-centric. When I have to use "Ctrl-hover" to get
some information, I won't use it.
You don't even have this functionality in Proof General, so it is hardly
a remaining reason for Proof General.
Again: after some weeks of practice, you will be much faster with jEdit
than Emacs. I always feel encumbered when I have to go back to Emacs for
- last time I checked, the 'abbreviation to unicode' conversion that
finally(!!) works great in PG, was somewhat unusable in jEdit.
Can you explain that feature of Proof General. I have never heard of it.
In Isabelle2013-1 the symbol completion mechanism has been generally
brushed up. Better forget what it was in Isabelle2013 or Proof General,
and experiment to see its possibilities. There is also some documentation
in the Isabelle/jEdit manual.
apart from old habits.
And this is also not to be underrated. Over the last two years, I have
compiled a 150 lines .emacs (and I'm only using Emacs for Isabelle) plus
some 'isabelle emacs' startup magic. Hence being urged to spend all this
time again to get the editor in a shape one likes, does not feel good.
Especially when there are NEWS items reading "you have to re-do all your
current jEdit keybinding customizations".
I can't do anything here. You need to be ready to give up old Emacs
things and move on to a brave new world. Isabelle/jEdit is not the
future, it is the present for quite some time already.
This archive was generated by a fusion of
Pipermail (Mailman edition) and