Coqtop always restarted when switching script buffer.

This comes from Hendrik's compile mode and is actually needed even
when this mode is off. When switching scripting buffer, restart the
coq shell process, so that it applies local coqtop options.

2 files changed, 12 insertions, 6 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 5a8c3af0..0f7c82af 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -654,10 +654,10 @@ 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)
+;; This is now always done (in coq.el)
+;(add-hook 'proof-deactivate-scripting-hook
+;          'coq-switch-buffer-kill-proof-shell
+;          t)
 
 
 (provide 'coq-compile-common)
diff --git a/coq/coq.el b/coq/coq.el
index a594bd49..f302d641 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2511,8 +2511,14 @@ are non-nil at the same time, this gives priority to the former."
   (let ((filename (concatenate 'string proof-home-directory "contrib/ML4PG/ml4pg.el")))
     (when (file-exists-p filename) (load-file filename) (ml4pg-select-mode))))
 
-
-
+;;;;;;;;;;;;;;
+
+;; This was done in coq-compile-common, but it is actually a good idea even
+;; when "compile when require" is off. When switching scripting buffer, let us
+;; restart the coq shell process, so that it applies local coqtop options. 
+(add-hook 'proof-deactivate-scripting-hook
+          'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
+          t)
 
 (provide 'coq)