diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-26 11:32:46 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-26 11:32:46 +0100 |
commit | cf290f2da6513c42ad57620136c7e6b6cebf8e11 (patch) | |
tree | b1114d17e8c507bae32520851b468d1ac4770232 /generic/proof-shell.el | |
parent | c6e44de22de8dfe7a5c9521201937a8302ec12c9 (diff) | |
parent | 4bcac92df46da9e68b5e3d565bb118fb63b4feb4 (diff) |
Merge branch 'master' of github.com:ProofGeneral/PG into master_origin
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r-- | generic/proof-shell.el | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 51038fa6..13da8d98 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -831,7 +831,11 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*). (let ((prover-was-busy nil)) (unless (proof-shell-live-buffer) (error "Proof process not started!")) - ;; hook functions might set prover-was-busy + ;; Hook functions might set prover-was-busy. + ;; In case `proof-action-list' is empty and only + ;; `proof-second-action-list-active' is t, the hook functions + ;; should clear the queue region and release the proof shell lock. + ;; `coq-par-user-interrupt' actually does this. (run-hooks 'proof-shell-signal-interrupt-hook) (if proof-shell-busy (progn |