diff options
| -rw-r--r-- | coq/coq-compile-common.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 10 |
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) @@ -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) |