If sent command fails, don't move the cursor.

[RafalKolanski]

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.

[David Aspinall]

Seems like a good idea, I agree... Not completely obvious that this is always what you want, though: imagine the case that the command doesn't fail immediately but takes some time. You have continued typing after the pink region while you wait. If the command fails, do you want the cursor to be suddenly thrown back? So to implement in a friendly way we might need a heuristic based on whether the user has typed or not.

I'll bump this for future consideration.

Meanwhile and anyway, have you seen this setting?

Options -> Follow Mode -> Never Move

You might find this easier to use than the default.

[RafalKolanski]

I tried turning on "Never Move". It still moves. (xemacs 21.4.20, PG 3.7pre I got from Isabelle 2007 distribution)

As for your other comment, if the command fails, I'd be perfectly fine with jumping to the location of where I was when I issued the command, even if I started typing elsewhere.

For a long term solution, your idea is better (keeping track of whether the user started typing).

[David Aspinall]

"Never Move" is now properly obeyed. You might like to mix the non-move behaviour with electric terminator, which now works without inserting a terminator character in Isabelle. It will move the cursor, but hopefully in a convenient and predictable way (like C-c C-n does when moving is enabled).