move some more material into coq-compile-common

1 files changed, 17 insertions, 1 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index bc7cf03f..081923a0 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -373,10 +373,26 @@ FILE should be an absolute file name. It can be nil if
     (append coq-prog-args (coq-include-options nil))))
 
 
-(provide 'coq-compile-common)
+;; kill coqtop on script buffer change
+
+(defun coq-switch-buffer-kill-proof-shell ()
+  "Kill the proof shell without asking the user.
+This function is for `proof-deactivate-scripting-hook'. It kills
+the proof shell without asking the user for
+confirmation (assuming she agreed already on switching the active
+scripting buffer). This is needed to ensure the load path is
+correct in the new scripting buffer."
+  (unless proof-shell-exit-in-progress
+    (proof-shell-exit t)))
+
 
+(add-hook 'proof-deactivate-scripting-hook
+          'coq-switch-buffer-kill-proof-shell
+          t)
 
 
+(provide 'coq-compile-common)
+
 ;;   Local Variables: ***
 ;;   coding: utf-8 ***
 ;;   End: ***