aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-09-21 14:31:09 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-09-21 14:31:09 +0000
commit4cffebeb11d5b2f02a6c26a7f4d40a90181586fc (patch)
tree8b1b2e746bc3dead3c8ed1625c0fccd8ee457714 /generic
parentccb6578324ca1c41340d532a32fc21036aee7576 (diff)
Callback for proof-shell-done-invisible now runs proof-state-change-hook.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-shell.el5
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3571b1d1..3adfbdf7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1418,8 +1418,9 @@ May be called by proof-shell-invisible-command."
(defun proof-shell-done-invisible (span)
- "Callback for proof-shell-invisible-command. Do nothing."
- ())
+ "Callback for proof-shell-invisible-command.
+Calls proof-state-change-hook."
+ (run-hooks 'proof-state-change-hook))
;; FIXME da: I find the name of this command misleading.
;; Nothing much is invisible really. Old docstring was