Call proof-state-change-hook after asserting and retracting.

1 files changed, 5 insertions, 5 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index f15bc477..487211cc 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -711,9 +711,9 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	   (funcall proof-global-p cmd)
 	   proof-lift-global
 	   (funcall proof-lift-global span)))))
-  ;; FIXME: circular dependency on proof-toolbar here!
-  (proof-toolbar-refresh)
-  )
+
+  ;; State of scripting may have changed now
+  (run-hooks 'proof-state-change-hook))
 
 
 
@@ -1053,8 +1053,8 @@ Optionally delete the region corresponding to the proof sequence."
 	(delete-spans start end 'type)
 	(delete-span span)
 	(if kill (kill-region start end))))
-  ;; FIXME: circular dependency on proof-toolbar here!
-  (proof-toolbar-refresh))
+  ;; State of scripting may have changed now
+  (run-hooks 'proof-state-change-hook))
 
 (defun proof-setup-retract-action (start end proof-command delete-region)
   (let ((span (make-span start end)))