diff options
author | Hendrik Tews <hendrik@askra.de> | 2012-11-03 13:20:22 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2012-11-03 13:20:22 +0000 |
commit | c3fafdf54d54c78124e76a72f4ecacb43dc5fcf1 (patch) | |
tree | 55a0a8d84cc9a061c05517470b471322c1f446ab /coq/coq-compile-common.el | |
parent | f9459e310ac9720e1da6c7025a1733c69b7b2a4b (diff) |
move another 2 functions into coq-compile-common
Diffstat (limited to 'coq/coq-compile-common.el')
-rw-r--r-- | coq/coq-compile-common.el | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 903663be..62ecfff4 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -373,6 +373,39 @@ FILE should be an absolute file name. It can be nil if (append coq-prog-args (coq-include-options nil)))) +;; ignore library files + +(defun coq-compile-ignore-file (lib-obj-file) + "Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE. +Return `t' if ProofGeneral should skip LIB-OBJ-FILE and `nil' if +ProofGeneral should handle the file. For normal users it does, for instance, +not make sense to let ProofGeneral check if the coq standard library +is up-to-date." + (or + (and + coq-compile-ignore-library-directory + (eq (compare-strings coq-library-directory 0 nil + lib-obj-file 0 (length coq-library-directory)) + t) + (if coq-debug-auto-compilation + (message "Ignore lib file %s" lib-obj-file)) + t) + (if (some + (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) + coq-compile-ignored-directories) + (progn + (if coq-debug-auto-compilation + (message "Ignore %s" lib-obj-file)) + t) + nil))) + +;; convert .vo files to .v files + +(defun coq-library-src-of-obj-file (lib-obj-file) + "Return source file name for LIB-OBJ-FILE. +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))) + ;; manage coq-compile-respose-buffer (defun coq-init-compile-response-buffer (command) |