put coq compilation feature into coq settings menu

4 files changed, 35 insertions, 20 deletions

diff --git a/coq/coq.el b/coq/coq.el
index af702775..9cf2c50a 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1113,11 +1113,14 @@ Currently this doesn't take the loadpath into account."
   :group 'coq
   :package-version '(ProofGeneral . "4.1"))
 
-(defcustom coq-compile-before-require nil
+(defpacustom compile-before-require nil
   "*If `t' check dependencies of required modules and compile if necessary.
 If `t' ProofGeneral intercepts \"Require\" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
-are compiled from the sources before the \"Require\" command is processed."
+are compiled from the sources before the \"Require\" command is processed.
+
+This option can be set/reset via menu
+`Coq -> Settings -> Compile Before Require'."
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
@@ -1144,17 +1147,20 @@ For instance, \"make -C %p %o\" expands to \"make -C bar foo.vo\"
 when module \"foo\" from directory \"bar\" is required.
 
 After the substitution the command can be changed in the
-minibuffer if `coq-confirm-external-compilation-command' is t."
+minibuffer if `coq-confirm-external-compilation' is t."
   :type 'string
   :safe '(lambda (v)
            (and (stringp v)
-                (or (not (boundp 'coq-confirm-external-compilation-command))
-                    coq-confirm-external-compilation-command)))
+                (or (not (boundp 'coq-confirm-external-compilation))
+                    coq-confirm-external-compilation)))
   :group 'coq-auto-compile)
 
-(defcustom coq-confirm-external-compilation-command t
+(defpacustom confirm-external-compilation t
   "*If set let user change and confirm the compilation command.
-Otherwise start the external compilation without confirmation."
+Otherwise start the external compilation without confirmation.
+
+This option can be set/reset via menu
+`Coq -> Settings -> Confirm External Compilation'."
   :type 'boolean
   :group 'coq-auto-compile)
 
@@ -1618,7 +1624,7 @@ function."
 Start a compilation to make ABSOLUTE-MODULE-OBJ-FILE up-to-date.
 The compilation command is derived from `coq-compile-command' by
 substituting certain keys, see `coq-compile-command' for details.
-If `coq-confirm-external-compilation-command' is t then the user
+If `coq-confirm-external-compilation' is t then the user
 must confirm the external command in the minibuffer, otherwise
 the command is executed without confirmation.
 
@@ -1641,7 +1647,7 @@ therefore the customizations for `compile' do not apply."
                 (car substitution) (eval (car (cdr substitution)))
                 local-compile-command)))
        coq-compile-substitution-list)
-      (if coq-confirm-external-compilation-command
+      (if coq-confirm-external-compilation
           (setq local-compile-command
                 (read-shell-command
                  "Coq compile command: " local-compile-command
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index a3bbd773..297b9641 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -3339,8 +3339,8 @@ which is the queue of things to do.
 additional properties are recorded as properties of @var{span}.
 
 @var{commands} is a list of strings, holding the text to be send to the
-prover. It might be the empty list is nothing needs to be sent to
-the prover, such as, for instance, for comments. Usually @var{commands}
+prover. It might be the empty list if nothing needs to be sent to
+the prover, such as, for comments. Usually @var{commands}
 contains just 1 string, but it might also contains more elements.
 The text should be obtained with
 @samp{(mapconcat }identity @var{commands} " ")', where the last argument
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e2795818..aa3a58a0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4048,7 +4048,7 @@ points to adhere to:
 @itemize @bullet
 @item
 The option @code{coq-compile-before-require} must be
-turned on.
+turned on (menu @code{Coq -> Settings -> Compile Before Require}).
 @item 
 Nonstandard load path elements @emph{must} be configured in the
 option @code{coq-load-path}. @code{-I} options in
@@ -4107,7 +4107,9 @@ general compilation facilities of Emacs
 (@inforef{Compilation,,emacs}) with its own customization variables.
 The compilation command must be customized in
 @code{coq-compile-command} and the flag
-@code{coq-confirm-external-compilation-command} determines
+@code{coq-confirm-external-compilation} (menu @code{Coq ->
+Settings -> Confirm External Compilation})
+determines
 whether the user must confirm the compilation command. The output
 of the compilation appears then in the @code{*compilation*}
 buffer.
@@ -4126,8 +4128,9 @@ Proof General cannot know if some library files have been updated
 outside of Proof General, therefore, it must perform the
 dependency checking for each @code{Require} command. If the
 continuous confirmation of the external compilation commands
-becomes tedious, set
-@code{coq-confirm-external-compilation-command} to nil.
+becomes tedious, disable
+@code{coq-confirm-external-compilation} (see menu @code{Coq ->
+Settings}).
 
 When a @code{Require} command causes a compilation of some files
 one may wish to save some buffers to disk beforehand. The option
@@ -4188,6 +4191,9 @@ If @samp{t} ProofGeneral intercepts "Require" commands and checks if the
 required library module and its dependencies are up-to-date. If not, they
 are compiled from the sources before the "Require" command is processed.
 
+This option can be set/reset via menu
+@samp{Coq -> Settings -> Compile Before Require}.
+
 The default value is @code{nil}.
 @end defopt
 
@@ -4216,17 +4222,20 @@ For instance, "make -C %p %o" expands to "make -C bar foo.vo"
 when module "foo" from directory "bar" is required.
 
 After the substitution the command can be changed in the
-minibuffer if @samp{@code{coq-confirm-external-compilation-command}} is t.
+minibuffer if @samp{@code{coq-confirm-external-compilation}} is t.
 
 The default value is @code{""}.
 @end defopt
 
 
-@c TEXI DOCSTRING MAGIC: coq-confirm-external-compilation-command
-@defopt coq-confirm-external-compilation-command 
+@c TEXI DOCSTRING MAGIC: coq-confirm-external-compilation
+@defopt coq-confirm-external-compilation 
 If set let user change and confirm the compilation command.@*
 Otherwise start the external compilation without confirmation.
 
+This option can be set/reset via menu
+@samp{Coq -> Settings -> Confirm External Compilation}.
+
 The default value is @code{t}.
 @end defopt
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 65c94d59..c70c4eaa 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -46,8 +46,8 @@ SPAN is a region in the sources, where COMMANDS come from. Often,
 additional properties are recorded as properties of SPAN.
 
 COMMANDS is a list of strings, holding the text to be send to the
-prover. It might be the empty list is nothing needs to be sent to
-the prover, such as, for instance, for comments. Usually COMMANDS
+prover. It might be the empty list if nothing needs to be sent to
+the prover, such as, for comments. Usually COMMANDS
 contains just 1 string, but it might also contains more elements.
 The text should be obtained with
 `(mapconcat 'identity COMMANDS \" \")', where the last argument