2011/9/10 Erik Martin-Dorel <erik.martin-do...@ens-lyon.fr>:
> Hi,
> I would like to report three interrelated issues that I noticed in the
> current CVS version of ProofGeneral.
> ================
> 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?

> By the way, it is neither consistant with, e.g., the behavior of the
> interactive OCaml toplevel that we can run with [M-x run-caml].

Good question, is there a standard keybinding for process killing in emacs?

For example in compilation mode it is C-c C-k.

> ...
> 2. Moreover, the command [C-c C-x] does not take into account its
> optional argument DONT-ASK, which would be very useful either
> (namely, allowing the user to do [C-u C-c C-x] to skip the invocation
> of yes-or-no-p itself).
> To fix this, I believe
>> (defun proof-shell-exit (&optional dont-ask)
>>  (interactive)
>>  ...)
> should be replaced with
>> (defun proof-shell-exit (&optional dont-ask)
>>  (interactive "P")
>>  ...)

Thanks for this one it is commited in cvs.

> 3. Finally, it seems the function `proof-shell-exit' raises
> systematically an unexpected error.
> To reproduce it, run the (Coq) prover, then try:
> [M-: (setq debug-on-error t) RET]
> [C-c C-x]

I have noticed this too. This is recent. I have put this in trac.

Pierre Courtieu
ProofGeneral-devel mailing list

Reply via email to