proof-shell: Don't ask about killing the proof assistant on exit #793
Conversation
- add menu entry to disable splash screen to quick options - add info to the splash screen on how to leave and disable the splash screen - add Proof-General menu to splash screen, such that the hints on the splash screen make sense - fix saving of quick options for several options - the CHANGES entry also describes commit ea0f007 - adapt manual
| ;; If one quits Proof General, it's clear that the proof | ||
| ;; assistant needs to be killed - don't ask. |
There was a problem hiding this comment.
On the one hand I agree with your remark;
but on the other hand I believe changing would be not "uniform" w.r.t. other emacs features?
e.g. if we do M-x shell RET
then C-x C-s, exactly as you say, "if we quit emacs, it's clear that the nested shell needs to be killed", but emacs will still ask for confirmation.
Would you agree to customize this?
|
> + ;; If one quits Proof General, it's clear that the proof
> + ;; assistant needs to be killed - don't ask.
[ Nitpick: the flag affects the behavior when one quits Emacs, rather
than Proof General. I don't think we even have a clear notion of
"quitting Proof General". ]
e.g. if we do `M-x shell RET`
then `C-x C-s`, exactly as you say, "if we quit Emacs, it's clear that the
nested shell needs to be killed", but Emacs will still ask for confirmation.
I'm not sure which behavior is better here (my own use of Coq is
sufficiently limited that I don't think it's representative), but the
main issue is whether killing the process would lose information, IOW
it's whether the state of the process is likely to contain information
that the user cannot trivially recreate (e.g. by restarting the process).
For `M-x shell` we consider that it's sufficiently common to have such
important state (for example because the shell is currently running
a command whose interruption would leave a mess).
|
|
@monnier thanks for your feedback! regarding your main point:
it appears than unlike |
|
Being in favour of the change. |
This PR is only about the commit in the title. To avoid conflicts, it builds on PR #791.
I have disabled this silly question about killing Coq when quitting Emacs decades ago already. IMO we don't need a user option to control this behavior.