move ancestor locking/unlocking to coq-compile-common

1 files changed, 32 insertions, 0 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1e10f0dd..ead28e22 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -408,6 +408,38 @@ is up-to-date."
 Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"."
   (substring lib-obj-file 0 (- (length lib-obj-file) 1)))
 
+
+;; ancestor (un-)locking
+
+(defun coq-lock-ancestor (span ancestor-src)
+  "Lock ancestor ANCESTOR-SRC and register it in SPAN.
+Lock only if `coq-lock-ancestor' is non-nil. Further, do nothing,
+if ANCESTOR-SRC is already a member of
+`proof-included-files-list'. Otherwise ANCESTOR-SRC is locked and
+registered in the 'coq-locked-ancestors property of the SPAN to
+properly unlock ANCESTOR-SRC on retract."
+  (if coq-lock-ancestors
+      (let ((true-ancestor-src (file-truename ancestor-src)))
+        (unless (member true-ancestor-src proof-included-files-list)
+          (proof-register-possibly-new-processed-file true-ancestor-src)
+          (span-set-property
+           span 'coq-locked-ancestors
+           (cons true-ancestor-src
+                 (span-property span 'coq-locked-ancestors)))))))
+
+(defun coq-unlock-ancestor (ancestor-src)
+  "Unlock ANCESTOR-SRC."
+  (let* ((true-ancestor (file-truename ancestor-src)))
+    (setq proof-included-files-list
+          (delete true-ancestor proof-included-files-list))
+    (proof-restart-buffers (proof-files-to-buffers (list true-ancestor)))))
+
+(defun coq-unlock-all-ancestors-of-span (span)
+  "Unlock all ancestors that have been locked when SPAN was asserted."
+  (mapc 'coq-unlock-ancestor (span-property span 'coq-locked-ancestors))
+  (span-set-property span 'coq-locked-ancestors ()))
+
+
 ;; manage coq-compile-respose-buffer
 
 (defun coq-init-compile-response-buffer (command)