diff options
author | Hendrik Tews <hendrik@askra.de> | 2011-09-14 19:18:04 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2011-09-14 19:18:04 +0000 |
commit | 1faf69c4bac18a7386f098a9ce3221e01476871d (patch) | |
tree | a047349b0889d3da4160388ee1139a3884357c61 /generic/proof-shell.el | |
parent | 96fe322d111bf21a75343afab39d76785f9b29e7 (diff) |
fix #421 with solution 1
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r-- | generic/proof-shell.el | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 756aa4da..b4ef6d84 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -110,6 +110,12 @@ The previous output is held back for processing at end of queue.") This ensures that the proof queue will be interrupted even if no interrupt message is printed from the prover after the last output.") +(defvar proof-shell-exit-in-progress nil + "A flag indicating that the current proof process is about to exit. +This flag is set for the duration of `proof-shell-kill-function' +to tell hooks in `proof-deactivate-scripting-hook' to refrain +from calling `proof-shell-exit'.") + ;; @@ -423,6 +429,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (redisplay t) (when (and alive proc) (catch 'exited + (setq proof-shell-exit-in-progress t) (set-process-sentinel proc (lambda (p m) (throw 'exited t))) @@ -469,6 +476,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (when (buffer-live-p (symbol-value buf)) (kill-buffer (symbol-value buf)) (set buf nil)))) + (setq proof-shell-exit-in-progress nil) (message "%s exited." bufname))) (defun proof-shell-clear-state () @@ -497,7 +505,11 @@ argument DONT-ASK is non-nil, the proof process is terminated without confirmation. The kill function uses `<PA>-quit-timeout' as a timeout to wait -after sending `proof-shell-quit-cmd' before rudely killing the process." +after sending `proof-shell-quit-cmd' before rudely killing the process. + +This function should not be called if +`proof-shell-exit-in-progress' is t, because a recursive call of +`proof-shell-kill-function' will give strange errors." (interactive "P") (if (buffer-live-p proof-shell-buffer) (when (or dont-ask |