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! 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]. I propose two different suggestions: 1.1. Get back to the previous standard behavior, namely remove in generic/proof-shell.el:
;; PG manages the prover process, don't query user on exit (set-process-query-on-exit-flag (get-buffer-process proof-shell-buffer) nil)
The advantage of the previous behavior is is that it prevents the user from inadvertently shutdown his session. 1.2. Otherwise, in order to make both behaviors possible, create a custom option `proof-query-on-exit' and a function with the same name that updates the flag accordingly. ================ 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") ...)
================ 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] ================ Hoping you will be able fixing these issues for the pending release. Kind regards, Erik PS: I use Coq-8.3pl2 and GNU Emacs 23.3.1 -- Érik Martin-Dorel PhD student, ENS de Lyon, LIP http://perso.ens-lyon.fr/erik.martin-dorel/ _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
