- implemented coq-lock-ancestors as described in the docs already

3 files changed, 37 insertions, 11 deletions

diff --git a/coq/coq.el b/coq/coq.el
index c4b77a41..19e8dd62 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1095,6 +1095,8 @@ Currently this doesn't take the loadpath into account."
 ;;
 
 ;; TODO list:
+;; - restart coqtop on buffer switch
+;; - update patch website
 ;; - display coqdep errors in the recompile-response buffer
 ;; - use a variable for the recompile-response buffer
 ;; - fix problem with partial library names
@@ -1183,6 +1185,14 @@ confirmation."
     (const :tag "save all buffers without confirmation" save-all))
   :group 'coq-auto-compile)
 
+(defcustom coq-lock-ancestors t
+  "*If t lock ancestor module files.
+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
+  :group 'coq-auto-compile)
+
 (defcustom coq-compile-ignore-library-directory t
   "*If `t' ProofGeneral does not compile modules from the coq library.
 Should be `t' for normal coq users. If `nil' library modules are
@@ -1475,7 +1485,9 @@ function."
             (message "coq-auto-compile: no source file for %s" lib-obj-file)
             (setq result
                   ;; 5 value: last modification time
-                  (nth 5 (file-attributes lib-obj-file))))))
+                  (nth 5 (file-attributes lib-obj-file))))
+          (if coq-lock-ancestors
+              (proof-register-possibly-new-processed-file lib-src-file))))
       ;; at this point the result value has been determined
       ;; store it in the hash then
       (puthash lib-obj-file result coq-obj-hash)
@@ -1503,7 +1515,10 @@ to save all buffers without confirmation before compilation."
                 (car substitution) (eval (car (cdr substitution)))
                 compile-command)))
        coq-compile-substitution-list)
-      (call-interactively 'compile))))
+      (call-interactively 'compile)
+      (if coq-lock-ancestors
+          (proof-register-possibly-new-processed-file
+           (coq-library-src-of-obj-file absolute-module-obj-file))))))
 
 (defun coq-map-module-id-to-obj-file (module-id)
   "Map MODULE-ID to the appropriate coq object file.
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index c774200f..d97e32d7 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -2384,7 +2384,7 @@ can be achieved via two hook functions which are run before and after
 fontifying the output buffers.
 
 @c TEXI DOCSTRING MAGIC: proof-zap-commas
-@defun proof-zap-commas limit
+@defun proof-zap-commas 
 Remove the face of all @samp{,} from point to @var{limit}.@*
 Meant to be used from @samp{@code{font-lock-keywords}} as a way
 to unfontify commas in declarations and definitions.
@@ -2581,7 +2581,7 @@ To insert text into the current (usually script) buffer, the function
 
 
 @c TEXI DOCSTRING MAGIC: proof-insert
-@defun proof-insert text
+@defun proof-insert 
 Insert @var{text} into the current buffer.@*
 @var{text} may include these special characters:
 @lisp
@@ -2651,7 +2651,7 @@ Define command FN to prompt for string @var{cmdvar} to proof assistant.@*
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-format-filename
-@defun proof-format-filename string filename
+@defun proof-format-filename 
 Format @var{string} by replacing quoted chars by escaped version of @var{filename}.
 
 %e uses the canonicalized expanded version of filename (including
@@ -2900,14 +2900,14 @@ behaviour and appearance for boolean user options, as well as
 interfacing properly with the @code{customize} mechanism.
 
 @c TEXI DOCSTRING MAGIC: proof-set-value
-@defun proof-set-value sym value
+@defun proof-set-value 
 Set a customize variable using @samp{@code{set-default}} and a function.@*
-We first call @samp{@code{set-default}} to set @var{sym} to @var{value}.
-Then if there is a function @var{sym} (i.e. with the same name as the
-variable @var{sym}), it is called to take some dynamic action for the new
+We first call @samp{@code{set-default}} to set SYM to @var{value}.
+Then if there is a function SYM (i.e. with the same name as the
+variable SYM), it is called to take some dynamic action for the new
 setting.
 
-If there is no function @var{sym}, we try stripping
+If there is no function SYM, we try stripping
 @samp{@code{proof-assistant-symbol}} and adding "proof-" instead to get
 a function name.  This extends @code{proof-set-value} to work with
 generic individual settings.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 98dc87ae..3a10d485 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4154,6 +4154,17 @@ The default value is @code{ask-coq}.
 @end defopt
 
 
+@c TEXI DOCSTRING MAGIC: coq-lock-ancestors
+@defopt coq-lock-ancestors 
+If t lock ancestor module files.@*
+If external compilation is used (via @samp{@code{coq-compile-command}}) then
+only the direct ancestors are locked. Otherwise all ancestors are
+locked when the "Require" command is processed.
+
+The default value is @code{t}.
+@end defopt
+
+
 The following two options deal with the load path. Proof General
 divides the load path into the standard load path (which is
 hardwired in the tools and need not be set explicitly), the
@@ -4479,7 +4490,7 @@ at the top of your theory file, like this:
 The default value is @code{nil}.
 @end defopt
 @c TEXI DOCSTRING MAGIC: isabelle-choose-logic
-@deffn Command isabelle-choose-logic logic
+@deffn Command isabelle-choose-logic 
 Adjust isabelle-prog-name and @code{proof-prog-name} for running @var{logic}.
 @end deffn
 @node Isabelle commands