2011/9/10 Erik Martin-Dorel <[email protected]>: > 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. Best, Pierre Courtieu _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
