[nongnu] elpa/proof-general ab510c61e2 3/4: Merge pull request #656 from hendriktews/opam-aware

[ELPA Syncer]

branch: elpa/proof-general
commit ab510c61e22ecacea7cbbf7de8d559f3dbda22e8
Merge: 0ee2b75939 a3d0fc9875
Author: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Commit: GitHub <noreply@github.com>

    Merge pull request #656 from hendriktews/opam-aware
    
    Close #210
---
 CHANGES                   |  7 ++++++
 coq/coq-compile-common.el | 18 ----------------
 coq/coq.el                | 54 +++++++++++++++++++++++++++++++++++++++++------
 doc/ProofGeneral.texi     | 36 +++++++++++++++++++++++++++++++
 4 files changed, 90 insertions(+), 25 deletions(-)

diff --git a/CHANGES b/CHANGES
index 0c45024b8c..bfce6dcd85 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 ProofGeneral/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
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index f7748846f0..bb51dbb55b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4187,6 +4187,7 @@ assistant.  It supports most of the generic features of 
Proof General.
 * Holes feature::
 * Proof-Tree Visualization::
 * Showing Proof Diffs::
+* Opam-switch-mode support::
 @end menu
 
 
@@ -5320,6 +5321,41 @@ have added or removed tokens are shown with the entire 
line highlighted with
 a @code{Coq Diffs ... Bg} face.  The added or removed tokens themselves are 
highlighted
 with non-@code{Bg} faces.
 
+@node Opam-switch-mode support
+@section Opam-switch-mode support
+
+Coq can be installed using @code{opam} (the OCaml package manager),
+which makes it easy to manage several different switches, having each
+a different version of Coq.
+
+Instead of running a command like @code{opam switch ...} in a terminal
+and restarting emacs to benefit from a different switch, one can:
+
+@itemize @bullet
+@item
+@b{Install} the
+@uref{https://github.com/ProofGeneral/opam-switch-mode,
+opam-switch-mode} and use the dedicated mode bar menu @code{OPSW} it
+provides.
+@item
+@b{Configure} Proof General using the customization option
+@code{coq-kill-coq-on-opam-switch}, so that the Coq background process
+is killed when changing the opam switch through
+@code{opam-switch-mode}.
+@end itemize
+
+@c TEXI DOCSTRING MAGIC: coq-kill-coq-on-opam-switch
+@defvar coq-kill-coq-on-opam-switch 
+If t kill coq when the opam switch changes (requires 
@samp{opam-switch-mode}).@*
+When @samp{opam-switch-mode} is loaded and the user changes the opam switch
+through @samp{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 
@samp{opam-switch-mode}
+@end defvar
+
 @c =================================================================
 @c
 @c  CHAPTER: EasyCrypt Proof General