aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-22 09:54:03 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-22 09:54:03 +0000
commitb9f01954505cc102ac49ddbd71e366dcd078472b (patch)
tree16c1ba61328c9d625ae5c768128d90b4949967bb /generic
parentb794c9734b99a9e7165472c70a15e8f5442de1a9 (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.el8
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