Re: [isabelle] Remaining reasons for Proof General



Hallo,

if it is in interests, here are the reasons why I do not use jEdit:

1. Automatic Processing
By this I mean that jEdit always processes the proof text at the cursor
position. I know this is supposed to be a feature of jEdit, but I just
find it annoying. I like my prover to be in a fixed state that I can
alter when I want to. Particularly when you have proof text that takes a
long time to process (e.g. due to large terms, I had that in programme
refinement a lot), one does not want jEdit to keep processing stuff that
it should leave alone for the moment.

2. Unicode Tokens
In Proof General, I type "ALL" and I get a "∀". In jEdit, I type "all",
I get an annoying popup and have to confirm my choice with a key press.
I have tried to get used to this, but I cannot, even after setting the
popup delay to 0 and adding Space and Tab as keys for confirming the
currently selected symbol. This is particularly tedious if one types a
sequence of symbols. In a way, I feel that users who /know/ their
unicode token names by heart are slowed down by unnecessary GUI (the
popup). I'd like to be able to switch it off and fall back to a Proof
General-like mechanism where I can type "ALL", "==>" and "\<alpha>" and
they are immediately converted to the corresponding Unicode token.

I could probably live with the first "problem"; but the second one is
really annoying; I just find that it slows down the speed at which I can
write proofs to great extent.

I am no friend of emacs and Proof General certainly has its problem, so
I have tried to switch to jEdit twice in the past, but the above two
things and the crashes and lags have led me back to Proof General; maybe
these are fixed now and I should try it again.

In this context, what is the point of "Sidekick"? It displays every
"have", every "using", every "by" as a single node?

Cheers,
Manuel


On 11/11/13 15:59, Makarius wrote:
> On Mon, 11 Nov 2013, Andreas Lochbihler wrote:
>
>>> People who are still using Proof General should say more explicitly
>>> what are the reasons
>>> for it, apart from old habits.
>> I use both jEdit and Proof General, but for different purposes. I see
>> the following advantages of ProofGeneral 3.7.1.1 with XEmacs:
>
> With some years of delay, that is a start. I don't see any fundamental
> problems in this list, just accidental behaviour which can be easily
> tuned or done differently.
>
> You know yourself that XEmacs / ProofGeneral 3.7.1.1 is totally
> obsolete. Current GNU Emacs is at version 24 and Proof General 4.2. I
> wonder if there are other remaining users of ProofGeneral 3.7.1.1.
>
>
>> With jEdit, I have to switch to the mouse far more often, in
>> particular for sledgehammer, find_theorems and to navigate from one
>> theory file to another.
>
> jEdit has quite smart keyboard shortcuts for many things, but they are
> usually quite different from Emacs. Switching files works via the
> "buffer switcher", which is keyboard operable (a bit difficult on
> German layouts, though). After several weeks of practice, operating
> jEdit should be much faster than Emacs.
>
> The Find and Sledgehammer panel are my own responsibility, and they
> are new in Isabelle2013-1, so more refinements can be expected. There
> are already jEdit actions to open the dockable windows, which also
> puts the focus on the main GUI component to activate the tool in
> question via plain RETURN. Note that jEdit "actions" can be mapped to
> keyboard shortcuts by the user. This is not done by default, to avoid
> the "Escape Meta Alt Control Shift" syndrome.
>
>
>> Similarly, I often want to look somewhere else in my theory file (and
>> use PgUp/PgDn for that); with ProofGeneral, I just type C-c C-. to
>> get back to where I was before, but I do not know an equally simple
>> way in jEdit.
>
> Isn't that just abuse of the accidental boundary between checked and
> unchecked text? This "focus" no longer exists in Isabelle/jEdit
> anyway, which is actually one of the main points of the whole approach.
>
> What jEdit (or Isabelle/jEdit) really needs is nice navigation support
> in the sense of Firefox or similar. One mainly needs to work out a
> good scheme when or how to "commit" positions to the navigation
> history, and maybe brush up the existing Navigator plugin.
>
>
>> 2. XEmacs has less spacing between the lines (this is the main reason
>> why I still use ProofGeneral 3.7.1.1, GNU Emacs with PG 4.x has a
>> similar spacing as jEdit), so more of the proof script fits on the
>> screen at the same font size.
>
> That is a question about fonts. In principle you can use alternative
> fonts in jEdit to your liking, although I consider IsabelleText the
> best compromise for display quality and glyph coverage.
>
> Note that jEdit has an option for extra vertical line spacing (Global
> Options / Text Area). I've never used it myself, but it could work out
> reasonably well. If not, it is relatively easy to tune that text
> painting, because I am doing it all myself anyway.
>
>
> In XEmacs you still have bitmap fonts. I wonder if/how it survives a
> switch to high-definition displays that have become available in the
> mass marked last year. Gladly, Oracle has already managed to catch up,
> notably with Apple's Retina in Jdk-7u40, so jEdit is already beyond
> the dividing line of current and obsolete applications. My cheap Sony
> HD display also works nicely with jEdit fonts.
>
>
>> 3. The output buffers are not usable with a key board. This is
>> particularly annoying when I examine diagnostic output as produced by
>> code_thms, export_code, print_classes, thm <large Named_THM
>> collection>, etc. In jEdit, I first have to open a new buffer and
>> copy the output there before I can use search and friends to navigate
>> through.
>
> The Output panel is not a buffer at all, but a dockable window. It
> re-uses some of the jEdit buffer display technology, but there is no
> attempt to imitate Emacs where "everything is a buffer". The latter
> approach sometimes has advantages, sometimes disadvantages. Like Proof
> General stayed faithful how Emacs works, Isabelle/jEdit takes jEdit
> customs seriously.
>
> Searching in Output panels should not be a fundamental problem. It is
> just one of the many small things that did not yet make into
> Isabelle/jEdit, because time was spent instead to maintain Proof General.
>
>
>> 4. After a few hours of work, jEdit reacts slower and slower. This
>> gets particularly annoying when typing fast. For example, I want that
>> entering < = TAB produces the \<le> symbol, always. Half of the time,
>> I am faster than the popup and I get "<= " instead.
>
> I have never heard of that. There might be a serious problem behind it
> that needs to be investigated. Problems that are known can be solved
> eventually. Secret ones will remain forever.
>
>
> Makarius
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.