- mark new coq specific variables as safe

- hint on per-directory local variables

2 files changed, 25 insertions, 3 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 516125a8..49106827 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1124,6 +1124,7 @@ 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."
   :type 'boolean
+  :safe 'booleanp
   :group 'coq-auto-compile)
 
 (defcustom coq-compile-command ""
@@ -1145,6 +1146,7 @@ the following keys are substituted as follows:
 For instance, \"make -C %p %o\" expands to \"make -C bar foo.vo\"
 when module \"foo\" from directory \"bar\" is required."
   :type 'string
+  :safe 'stringp
   :group 'coq-auto-compile)
 
 (defconst coq-compile-substitution-list
@@ -1187,6 +1189,7 @@ confirmation."
      "save all coq-mode buffers except the current buffer without confirmation"
      save-coq)
     (const :tag "save all buffers without confirmation" save-all))
+  :safe '(lambda (v) (member v '(ask-coq ask-all save-coq save-all)))
   :group 'coq-auto-compile)
 
 (defcustom coq-lock-ancestors t
@@ -1195,6 +1198,7 @@ If external compilation is used (via `coq-compile-command') then
 only the direct ancestors are locked. Otherwise all ancestors are
 locked when the \"Require\" command is processed."
   :type 'boolean
+  :safe 'booleanp
   :group 'coq-auto-compile)
 
 (defcustom coq-compile-ignore-library-directory t
@@ -1206,6 +1210,7 @@ This option has currently no effect, because Proof General uses
 coqdep to translate qualified identifiers into library file names
 and coqdep does not output dependencies in the standard library."
   :type 'boolean
+  :safe 'booleanp
   :group 'coq-auto-compile)
 
 (defcustom coq-compile-ignored-directories nil
@@ -1218,6 +1223,7 @@ compilation. It makes sense to include non-standard coq library
 directories here if they are not changed and if they are so big
 that dependency checking takes noticeable time."
   :type '(repeat regexp)
+  :safe '(lambda (v) (every 'stringp v))
   :group 'coq-auto-compile)
 
 (defcustom coq-load-path nil
@@ -1232,6 +1238,7 @@ For coqdep and coqc these directories are passed via \"-I\"
 options over the command line. For interactive scripting an
 \"Add LoadPath\" command is used."
   :type '(repeat string)
+  :safe '(lambda (v) (every 'stringp v))
   :group 'coq-auto-compile)
 
 (defcustom coq-load-path-include-current t
@@ -1240,6 +1247,7 @@ Should be `t' for normal users. If `t' pass \"-I dir\" to coqdep when
 processing files in directory \"dir\" in addition to any entries
 in `coq-load-path'."
   :type 'boolean
+  :safe 'booleanp
   :group 'coq-auto-compile)
 
 (defconst coq-require-command-regexp
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 1cc65a33..6cf876b1 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3757,7 +3757,7 @@ and a short-cut for enabling three window mode,
 @cindex file variables
 
 A very convenient way to customize file-specific variables is to use 
-File Variables (@inforef{File Variables, ,(emacs)}). This feature of
+File Variables (@inforef{File Variables, ,emacs}). This feature of
 Emacs permits to specify values for certain Emacs variables
 when a file is loaded. File variables and their values 
 are written as a list at the end of
@@ -3782,8 +3782,8 @@ end of @file{foo.v}:
 This way, the right command line arguments are passed to the
 invocation of
 @code{coqtop} when scripting starts in
-@file{foo.v}. We assume here that the load path @code{"../theories"}
-is specific to the file @file{foo.v}, and that therefore a global
+@file{foo.v}. Note that the load path @code{"../theories"} is
+project or even file specific, and that therefore a global
 setting via the
 configuration tool would be inappropriate.
 With file variables, Emacs will set @code{coq-load-path}
@@ -3811,6 +3811,20 @@ compile} command. Note that the lines are commented in order to be
 ignored by the proof assistant. It is possible to use this mechanism for
 all variables, @inforef{File Variables, ,emacs}.
 
+One can also specify file variables on a per directory basis,
+@inforef{Directory Variables, ,emacs}. For instance,
+assume you have a Coq project with several subdirectories and you
+want to put each subdirectory into @code{coq-load-path} for every
+file in the project. You can achieve this by storing
+
+@lisp
+((coq-mode . ((coq-load-path . ("../dir_1" "../dir_2" ... )))))
+@end lisp
+
+into the file @code{.dir-locals.el} in one of the parent
+directories. The value in this file must be an alist that maps
+mode names to alists, where these latter alists map variables to
+values, @inforef{Directory Variables, ,emacs}.