Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-14 Thread David Aspinall
Hi Hendrik Thanks for the discussion on this: If nobody objects, I'll adopt solution 1 (see #421 for solution 2): Inside proof-shell-kill-function set a global variable proof-shell-exit-in-progress. When coq-switch-buffer-kill-proof-shell sees this it refrains from calling

Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-12 Thread Hendrik Tews
Pierre Courtieu pierre.court...@cnam.fr writes: 2011/9/10 Erik Martin-Dorel erik.martin-do...@ens-lyon.fr: 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

Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-11 Thread Tom Prince
On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieu pierre.court...@cnam.fr wrote: 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

Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

2011-09-11 Thread Erik Martin-Dorel
Hello, On 09/11/2011 04:30 PM, Tom Prince wrote: On Sun, 11 Sep 2011 14:59:14 +0200, Pierre Courtieupierre.court...@cnam.fr wrote: 2011/9/10 Erik Martin-Dorelerik.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