[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 48ab233ea7 1/4: coq: make Proof General/coq
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general 48ab233ea7 1/4: coq: make Proof General/coq opam-switch-mode aware |
Date: |
Wed, 13 Jul 2022 12:59:01 -0400 (EDT) |
branch: elpa/proof-general
commit 48ab233ea7e317a5fa0875a462a6a711d91c6392
Author: Hendrik Tews <hendrik@askra.de>
Commit: Hendrik Tews <hendrik@askra.de>
coq: make Proof General/coq opam-switch-mode aware
See `coq-kill-coq-on-opam-switch`: Proof General can now reset
the proof shell when the opam switch is changed via
opam-switch-mode.
---
CHANGES | 7 ++++++
coq/coq-compile-common.el | 18 ----------------
coq/coq.el | 54 +++++++++++++++++++++++++++++++++++++++++------
3 files changed, 54 insertions(+), 25 deletions(-)
diff --git a/CHANGES b/CHANGES
index 0c45024b8c..e20941ce12 100644
--- a/CHANGES
+++ b/CHANGES
@@ -108,6 +108,13 @@ standard support.
documentation of this variable for an explanation of the different
possible values and some more information.
+*** Make Proof General/Coq `opam-switch-mode` aware
+
+ When opam-switch-mode is loaded, the Coq background process can be
+ killed when changing the opam switch through opam-switch-mode, see
+ `coq-kill-coq-on-opam-switch` and
+ https://github.com/ProofGeneral/opam-switch-mode.
+
*** Limited extensibility for indentation
Coq indentation mechanism is based on a fixed set of tokens and
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1055c7443e..8074d7faf1 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -798,24 +798,6 @@ current buffer (which contains the Require command) to
(save-some-buffers unconditionally buffer-filter)))
-;;; 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)))
-
-;; 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)
;; Local Variables: ***
diff --git a/coq/coq.el b/coq/coq.el
index c8d92ca7e4..5a85bf7b9d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3422,15 +3422,55 @@ priority to the former."
(put 'coq-terminator-insert 'delete-selection t)
-;;;;;;;;;;;;;;
-;; 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)
+;;;;;;;;;;;;;; kill coq background process on different occasions
;;;;;;;;;;;;;;
+
+;; This originates from background compilation, 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.
+
+(defun coq-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-kill-proof-shell t)
+
+(defcustom coq-kill-coq-on-opam-switch t
+ "If t kill coq when the opam switch changes (requires `opam-switch-mode').
+When `opam-switch-mode' is loaded and the user changes the opam switch
+through `opam-switch-mode' then this option controls whether the coq
+background process (the proof shell) is killed such that the next
+assert command starts a new proof shell, probably using a
+different coq version from a different opam switch.
+
+See https://github.com/ProofGeneral/opam-switch-mode for `opam-switch-mode'"
+ :type 'boolean
+ :group 'coq)
+
+
+(defun coq-kill-proof-shell-on-opam-switch ()
+ "Kill proof shell when the opam switch changes (requires `opam-switch-mode').
+This function is for the `opam-switch-mode' hook
+`opam-switch-change-opam-switch-hook', which runs when the user
+changes the opam switch through `opam-switch-mode'. If
+`coq-kill-coq-on-opam-switch' is t, then the proof shell is
+killed such that the next assert starts a new proof shell, using
+coq from the new opam switch."
+ (when (and coq-kill-coq-on-opam-switch proof-script-buffer)
+ (coq-kill-proof-shell)))
+
+
+(add-hook 'opam-switch-change-opam-switch-hook
+ #'coq-kill-proof-shell-on-opam-switch t)
+;;;;;;;;;;;;;;;
;; overwriting the default behavior, this is an experiment, *frames* will be
;; deleted only if only displaying associated buffers. If this is OK the