[isabelle] Remaining reasons for Proof General
On Mon, 11 Nov 2013, Andreas Lochbihler wrote:
People who are still using Proof General should say more explicitly what
are the reasons
I use both jEdit and Proof General, but for different purposes. I see the
following advantages of ProofGeneral 184.108.40.206 with XEmacs:
for it, apart from old habits.
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 220.127.116.11 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 18.104.22.168.
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
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 22.214.171.124, 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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and