On 09/11/2011 04:30 PM, Tom Prince wrote:
On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu<pierre.court...@cnam.fr>  
2011/9/10 Erik Martin-Dorel<erik.martin-do...@ens-lyon.fr>:
1. Now the behavior of [C-x C-c] is not really consistent with the one of
[C-c C-x].
Indeed, the second command calls yes-or-no-p before killing the
prover, while the first one now exits Emacs silently!

Hello, I don't understand this remark. The keybinging [C-x C-c] has
nothing to do with proofgeneral. It is the standard emacs keybinding
to exit emacs silently. Why C-c C-x should be consistent with it?

I think the issue is that with just proof-general open in emacs, and no
unsaved files, (and process-query-on-exit flag off), then C-c C-x
prompts about killing the prover, but that C-x C-c just silently kills
it and emacs.

Before, (with process-querry-on-exit-flag on), they would both prompt
before killing things (C-c C-x twice).


Indeed (except I don't think [C-c C-x] asked the question twice).

Moreover, I wanted to highlight the fact the behavior with flag ON that
Tom described is really uniform with standard Emacs interactive modes,
viz. [M-x shell] and [M-x run-caml],

and similarly [M-x compile], [M-x find-name] and [M-x rgrep] will ask
``Active processes exist; kill them and exit anyway? (yes or no)''
if one tries to exit Emacs while their process is running.

But if ever you had some personal reason to set this flag OFF,
I would thereby suggest to create a custom option `proof-query-on-exit'
and a function with the same name that updates the flag accordingly.

Kind regards,


√Črik Martin-Dorel
PhD student, ENS de Lyon, LIP
ProofGeneral-devel mailing list

Reply via email to