diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-22 09:54:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-22 09:54:03 +0000 |
| commit | b9f01954505cc102ac49ddbd71e366dcd078472b (patch) | |
| tree | 16c1ba61328c9d625ae5c768128d90b4949967bb /generic | |
| parent | b794c9734b99a9e7165472c70a15e8f5442de1a9 (diff) | |
Add proof-deactivate-scripting-hook. Also note activate-script-hook is no longer inherited
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 36214ff8..4369adfd 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1083,7 +1083,10 @@ a scripting buffer is killed it is always retracted." ;; not really necessary when called by kill buffer, at least. (if (fboundp 'redraw-modeline) (redraw-modeline) - (force-mode-line-update))))))) + (force-mode-line-update)) + + ;; Finally, run hooks (added in 3.5 22.04.04) + (run-hooks 'proof-deactivate-scripting-hook)))))) (defun proof-activate-scripting (&optional nosaves queuemode) "Ready prover and activate scripting for the current script buffer. @@ -2425,7 +2428,10 @@ command." (make-local-hook 'after-set-visited-file-name-hooks) (add-hook 'after-set-visited-file-name-hooks 'proof-script-set-visited-file-name)) + ;; FIXME 3.5: noticed 22.04.04 that 'proof-activate-scripting-hook is + ;; no longer inherited for some reason! (make-local-hook 'proof-activate-scripting-hook) + (make-local-hook 'proof-deactivate-scripting-hook) (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)) ;; NB: proof-mode-map declared by define-derived-mode above |