Re: [isabelle] sledgehammer in RC4

Dear Makarius,

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 with XEmacs:

1. XEmacs/ProofGeneral can be used completely without a mouse. 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.

2. Navigation by cursor keys is much slower. Moving a word to the left/right in XEmacs jumps to the beginning / end of the next word, where a word consists of at least one alphanumeric character. In jEdit, Ctrl-left/-right also stops at every parenthesis, white-space, operator and the like.

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.

2. XEmacs has less spacing between the lines (this is the main reason why I still use ProofGeneral, 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.

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.

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 tried this with 2013-1-RC3 last week, but not yet with RC4).

And finally, there's of course habits. I write my LaTeX documents in Emacs, so using the same editor with the same handling is very convenient.


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