Re: [isabelle] Remaining reasons for Proof General
Am 11.11.2013 18:13, schrieb Makarius:
> 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
> everytime afresh.
>> - 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 CPU).
> 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 2009.
Quadcore i7. Which should be fast enough... I'm using the gtk-style for
jEdit. Or I would need a high-end GPU ... (intel-whatever here only).
New testing on a second machine (which is slower) does not yield any
lags. Strange. Have to investigate.
>> - Fonts are not antialiased. I found that setting some obscure
>> environment variable  made it work, but honestly: no AA by default
>> is a no-go.
> Obsolete in Isabelle2013-1 and hardly an issue before, since it was well
> documented in the jEdit FAQ how to change such defaults.
Thanks. This indeed does work now.
>> - 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
My use case: Using PG with session X. Then noticing that I had to change
some theory in X. With session switching this was easy: Exit Isabelle,
switch session, restart isabelle (thereby building all of session X, but
for development this is ok).
With jEdit I would have to restart the editor.
>> - (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.
That's not a solution, but a workaround (I'm using the WM I'm using for
good reasons). The problem is not the WM, but Java, as it changed
behavior in Java7 and a new workaround in the WM had to be developed
(again: why Java is not just using existing techniques/libraries and is
doing everything from scratch itself, I do not understand).
But as already written: This problem is obsolete until the next JDK version.
>> - 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.
Typing e.g. /\ and getting \<and>, or |/ and getting \<^sub>.
But I just ran a fresh download on a previously isabelle-free computer
and it looked better than expected. Hence I'll give it a fresh try at
work (after having patched by WM) and will come back tomorrow (I'll also
ditch the gtk-style)
This archive was generated by a fusion of
Pipermail (Mailman edition) and