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 proof-shell-exit recursively.

I followed up on Trac.  I guess solution 2 would be better, but I don't
object if you prefer to implement solution 1.  

Best wishes,

 - David




-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel


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 debug-on-error t) RET]
[C-c C-x]

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

The problem is coq-switch-buffer-kill-proof-shell and that
proof-shell-kill-function does not take into account that a
prover might get killed when scripting is deactivated. For more
details see #421.

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 proof-shell-exit recursively.

Bye,

Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel


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
  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).

  Tom


___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel


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 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).

   Tom


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,

Erik

--
√Črik Martin-Dorel
PhD student, ENS de Lyon, LIP
http://perso.ens-lyon.fr/erik.martin-dorel/
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel