Custom Query (361 matches)

The commands of type (* comment *) and -- "comment" are absorbed as part of the previous command. They hardly ever describe the previous command, instead describing the *following* one.

I would much prefer if when I pressed "previous" or performed an undo using c-c c-return, I could go up to before the comment without undoing the previous command.

This is one of the reasons I've taken to working with strict read-only turned off, but for beginners this is not such a good idea.

When trying to undo a diagnostic command (such as thm) occurring inside a proof, as in

lemma "True"
  apply (rule TrueI)
  thm TrueI

ProofGeneral crashes with the error message "wrong-type-argument char-or-string-p nil". The error occurs with both XEmacs 21.4 and 21.5.

Init order in proof-shell-start is tricky, because the shell mode sets some configuration variables at the same time as the process is being fired up (and the proof-shell-config-done sends startup commands to the prover!).

This could be made cleaner by (1) creating the shell buffer and setting its mode first (including filter functions), then (2) firing up the comint process inside it, then finally (3) sending initialisation messages. It looks like the current comint interface would allow this to work correctly for derived modes, which may have been a problem in earlier versions.