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

1 files changed, 17 insertions, 2 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.