diff options
author | Hendrik Tews <hendrik@askra.de> | 2012-11-06 18:10:29 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2012-11-06 18:10:29 +0000 |
commit | d0774112051c18933eb75799e749e726d8f87efc (patch) | |
tree | 1b3bfdfcea8c859901e61d5c2f8ddd4522ca92ca /coq | |
parent | 7640cbe2fb2b6113725a15ddb5bf7acc9404d7ee (diff) |
move ancestor locking back into specific part
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-compile-common.el | 19 | ||||
-rw-r--r-- | coq/coq-seq-compile.el | 26 |
2 files changed, 25 insertions, 20 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index ead28e22..d66b52f5 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -409,23 +409,8 @@ 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))))))) +;;; ancestor unlocking +;;; (locking is different for sequential and parallel compilation) (defun coq-unlock-ancestor (ancestor-src) "Unlock ANCESTOR-SRC." diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 8437f803..f9543886 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -30,7 +30,27 @@ ;; Multiple file handling -- sequential compilation of required modules ;; -;; handle Require commands when queue is extended + +;;; ancestor locking +;;; (unlocking is shared in coq-compile-common.el) + +(defun coq-seq-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))))))) + +;;; handle Require commands when queue is extended (defun coq-seq-get-library-dependencies (lib-src-file &optional command-intro) "Compute dependencies of LIB-SRC-FILE. @@ -210,7 +230,7 @@ function." (setq result ;; 5 value: last modification time (nth 5 (file-attributes lib-obj-file)))) - (coq-lock-ancestor span lib-src-file))) + (coq-seq-lock-ancestor span 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) @@ -256,7 +276,7 @@ therefore the customizations for `compile' do not apply." ;; the next line is probably necessary to make recompile work (setq-default compilation-directory default-directory) (compilation-start local-compile-command) - (coq-lock-ancestor + (coq-seq-lock-ancestor span (coq-library-src-of-obj-file absolute-module-obj-file))))) |