Custom Query (361 matches)

Typical work flow is: change something, send using c-c c-return. If the command fails, it's probably due to the something I just changed, where I had the cursor in the first place. Unfortunately, proof general moves it to the end of the current command, making me have to go back manually, change things again, etc.

Being able to keep the cursor where it is if the command fails would be really nice.

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.