Re: [isabelle] sledgehammer in RC4
I use both jEdit and Proof General, but for different purposes. I see the following
advantages of ProofGeneral 126.96.36.199 with XEmacs:
People who are still using Proof General should say more explicitly what are the reasons
for it, apart from old habits.
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 188.8.131.52, 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