[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
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.