From 640f500daaf40e8e889f012bdfa7ad28719d256c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 30 Oct 2012 21:56:49 +0000 Subject: rename entities in coq-seq-compile --- coq/coq-seq-compile.el | 125 +++++++++++++++++++++++++------------------------ 1 file changed, 64 insertions(+), 61 deletions(-) (limited to 'coq/coq-seq-compile.el') diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 7e9e0bfd..cd2190bb 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -32,9 +32,9 @@ ;; ancestor (un-)locking -(defun coq-lock-ancestor (span ancestor-src) +(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, +Lock only if `coq-seq-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 @@ -48,21 +48,21 @@ properly unlock ANCESTOR-SRC on retract." (cons true-ancestor-src (span-property span 'coq-locked-ancestors))))))) -(defun coq-unlock-ancestor (ancestor-src) +(defun coq-seq-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) +(defun coq-seq-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)) + (mapc 'coq-seq-unlock-ancestor (span-property span 'coq-locked-ancestors)) (span-set-property span 'coq-locked-ancestors ())) ;; handle Require commands when queue is extended -(defun coq-compile-ignore-file (lib-obj-file) +(defun coq-seq-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, @@ -86,12 +86,12 @@ is up-to-date." t) nil))) -(defun coq-library-src-of-obj-file (lib-obj-file) +(defun coq-seq-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))) -(defun coq-init-compile-response-buffer (command) +(defun coq-seq-init-compile-response-buffer (command) "Initialize the buffer for the compilation output. If `coq-compile-response-buffer' exists, empty it. Otherwise create a buffer with name `coq-compile-response-buffer', put @@ -114,7 +114,7 @@ the command whose output will appear in the buffer." (with-current-buffer buffer-object (insert "-*- mode: compilation; -*-\n\n" command "\n"))))) -(defun coq-display-compile-response-buffer () +(defun coq-seq-display-compile-response-buffer () "Display the errors in `coq-compile-response-buffer'." (with-current-buffer coq-compile-response-buffer ;; fontification enables the error messages @@ -128,7 +128,7 @@ the command whose output will appear in the buffer." (save-selected-window (proof-resize-window-tofit window)))))) -(defun coq-get-library-dependencies (lib-src-file &optional command-intro) +(defun coq-seq-get-library-dependencies (lib-src-file &optional command-intro) "Compute dependencies of LIB-SRC-FILE. Invoke \"coqdep\" on LIB-SRC-FILE and parse the output to compute the compiled coq library object files on which @@ -169,25 +169,25 @@ break." (cons command-intro this-command) this-command))) ;; display the error - (coq-init-compile-response-buffer + (coq-seq-init-compile-response-buffer (mapconcat 'identity full-command " ")) (let ((inhibit-read-only t)) (with-current-buffer coq-compile-response-buffer (insert coqdep-output))) - (coq-display-compile-response-buffer) + (coq-seq-display-compile-response-buffer) "unsatisfied dependencies") (if (string-match ": \\(.*\\)$" coqdep-output) (cdr-safe (split-string (match-string 1 coqdep-output))) ())))) -(defun coq-compile-library (src-file) +(defun coq-seq-compile-library (src-file) "Recompile coq library SRC-FILE. Display errors in buffer `coq-compile-response-buffer'." (message "Recompile %s" src-file) (let ((coqc-arguments (nconc (coq-include-options src-file) (list src-file))) coqc-status) - (coq-init-compile-response-buffer + (coq-seq-init-compile-response-buffer (mapconcat 'identity (cons coq-compiler coqc-arguments) " ")) (if coq-debug-auto-compilation (message "call coqc arg list: %s" coqc-arguments)) @@ -200,14 +200,14 @@ Display errors in buffer `coq-compile-response-buffer'." (with-current-buffer coq-compile-response-buffer (buffer-string)))) (unless (eq coqc-status 0) - (coq-display-compile-response-buffer) + (coq-seq-display-compile-response-buffer) (let ((terminated-text (if (numberp coqc-status) "terminated with exit status" "was terminated by signal"))) (error "ERROR: Recompiling coq library %s %s %s" src-file terminated-text coqc-status))))) -(defun coq-compile-library-if-necessary (max-dep-obj-time src obj) +(defun coq-seq-seq-compile-library-if-necessary (max-dep-obj-time src obj) "Recompile SRC to OBJ if necessary. This function compiles SRC to the coq library object file OBJ if one of the following conditions is true: @@ -235,7 +235,7 @@ OBJ have identical modification times." (let (src-time obj-time) (if (eq max-dep-obj-time 'just-compiled) (progn - (coq-compile-library src) + (coq-seq-compile-library src) 'just-compiled) (setq src-time (nth 5 (file-attributes src))) (setq obj-time (nth 5 (file-attributes obj))) @@ -247,13 +247,13 @@ OBJ have identical modification times." ; which is newer than obj (time-less-p obj-time max-dep-obj-time))) (progn - (coq-compile-library src) + (coq-seq-compile-library src) 'just-compiled) (if coq-debug-auto-compilation (message "Skip compilation of %s" src)) obj-time)))) -(defun coq-make-lib-up-to-date (coq-obj-hash span lib-obj-file) +(defun coq-seq-make-lib-up-to-date (coq-obj-hash span lib-obj-file) "Make library object file LIB-OBJ-FILE up-to-date. Check if LIB-OBJ-FILE and all it dependencies are up-to-date compiled coq library objects. Recompile the necessary objects, if @@ -278,38 +278,41 @@ function." result) ;; lib-obj-file has not been checked -- do it now (message "Check %s" lib-obj-file) - (if (coq-compile-ignore-file lib-obj-file) + (if (coq-seq-compile-ignore-file lib-obj-file) ;; return minimal time for ignored files (setq result '(0 0)) (let* ((lib-src-file - (expand-file-name (coq-library-src-of-obj-file lib-obj-file))) + (expand-file-name + (coq-seq-library-src-of-obj-file lib-obj-file))) dependencies deps-mod-time) (if (file-exists-p lib-src-file) ;; recurse into dependencies now (progn - (setq dependencies (coq-get-library-dependencies lib-src-file)) + (setq dependencies + (coq-seq-get-library-dependencies lib-src-file)) (if (stringp dependencies) (error "File %s has %s" lib-src-file dependencies)) (setq deps-mod-time (mapcar (lambda (dep) - (coq-make-lib-up-to-date coq-obj-hash span dep)) + (coq-seq-make-lib-up-to-date coq-obj-hash span dep)) dependencies)) (setq result - (coq-compile-library-if-necessary + (coq-seq-seq-compile-library-if-necessary (coq-max-dep-mod-time deps-mod-time) lib-src-file lib-obj-file))) (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)))) - (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) result))) -(defun coq-auto-compile-externally (span qualified-id absolute-module-obj-file) +(defun coq-seq-auto-compile-externally (span qualified-id + absolute-module-obj-file) "Make MODULE up-to-date according to `coq-compile-command'. Start a compilation to make ABSOLUTE-MODULE-OBJ-FILE up-to-date. The compilation command is derived from `coq-compile-command' by @@ -324,11 +327,11 @@ span for for proper unlocking on retract. This function uses the low-level interface `compilation-start', therefore the customizations for `compile' do not apply." - (unless (coq-compile-ignore-file absolute-module-obj-file) + (unless (coq-seq-compile-ignore-file absolute-module-obj-file) (let* ((local-compile-command coq-compile-command) (physical-dir (file-name-directory absolute-module-obj-file)) (module-object (file-name-nondirectory absolute-module-obj-file)) - (module-source (coq-library-src-of-obj-file module-object)) + (module-source (coq-seq-library-src-of-obj-file module-object)) (requiring-file buffer-file-name)) (mapc (lambda (substitution) @@ -348,11 +351,11 @@ 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))))) + (coq-seq-library-src-of-obj-file absolute-module-obj-file))))) -(defun coq-map-module-id-to-obj-file (module-id span) +(defun coq-seq-map-module-id-to-obj-file (module-id span) "Map MODULE-ID to the appropriate coq object file. The mapping depends of course on `coq-load-path'. The current implementation invokes coqdep with a one-line require command. @@ -376,12 +379,12 @@ function returns () if MODULE-ID comes from the standard library." (with-temp-file temp-require-file (insert coq-string)) (setq result - (coq-get-library-dependencies + (coq-seq-get-library-dependencies temp-require-file (concat "echo \"" coq-string "\" > " temp-require-file)))) (delete-file temp-require-file)) (if (stringp result) - ;; Error handling: coq-get-library-dependencies was not able to + ;; Error handling: coq-seq-get-library-dependencies was not able to ;; translate module-id into a file name. We insert now a faked error ;; message into coq-compile-response-buffer to make next-error happy. (let ((error-message @@ -399,13 +402,13 @@ function returns () if MODULE-ID comes from the standard library." ;; (with-current-buffer (span-buffer span) ;; (line-number-at-pos (span-start span))) ;; error-message))) - ;; (coq-display-compile-response-buffer) + ;; (coq-seq-display-compile-response-buffer) (error error-message))) (assert (<= (length result) 1) - "Internal error in coq-map-module-id-to-obj-file") + "Internal error in coq-seq-map-module-id-to-obj-file") (car-safe result))) -(defun coq-check-module (coq-object-local-hash-symbol span module-id) +(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id) "Locate MODULE-ID and compile if necessary. If `coq-compile-command' is not nil the whole task of checking which modules need compilation and the compilation itself is done by an external @@ -419,65 +422,65 @@ for proper unlocking on retract. Argument COQ-OBJECT-LOCAL-HASH-SYMBOL provides a place to store the coq-obj-hash, which is used during internal -compilation (see `coq-make-lib-up-to-date'). This way one hash +compilation (see `coq-seq-make-lib-up-to-date'). This way one hash will be used for all \"Require\" commands added at once to the queue." - (let ((module-obj-file (coq-map-module-id-to-obj-file module-id span))) - ;; coq-map-module-id-to-obj-file currently returns () for + (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span))) + ;; coq-seq-map-module-id-to-obj-file currently returns () for ;; standard library modules! (when module-obj-file (if (> (length coq-compile-command) 0) - (coq-auto-compile-externally span module-id module-obj-file) + (coq-seq-auto-compile-externally span module-id module-obj-file) (unless (symbol-value coq-object-local-hash-symbol) (set coq-object-local-hash-symbol (make-hash-table :test 'equal))) - (coq-make-lib-up-to-date (symbol-value coq-object-local-hash-symbol) + (coq-seq-make-lib-up-to-date (symbol-value coq-object-local-hash-symbol) span module-obj-file))))) -(defvar coq-process-require-current-buffer - "Used in `coq-compile-save-some-buffers' and `coq-compile-save-buffer-filter'. +(defvar coq-seq-process-require-current-buffer + "Local variable for two coq-seq-* functions. This only locally used variable communicates the current buffer -from `coq-compile-save-some-buffers' to -`coq-compile-save-buffer-filter'.") +from `coq-seq-compile-save-some-buffers' to +`coq-seq-compile-save-buffer-filter'.") -(defun coq-compile-save-buffer-filter () - "Filter predicate for `coq-compile-save-some-buffers'. +(defun coq-seq-compile-save-buffer-filter () + "Filter predicate for `coq-seq-compile-save-some-buffers'. See also `save-some-buffers'. Returns t for buffers with major mode -'coq-mode' different from coq-process-require-current-buffer and nil +'coq-mode' different from coq-seq-process-require-current-buffer and nil for all other buffers. The buffer to test must be current." (and (eq major-mode 'coq-mode) - (not (eq coq-process-require-current-buffer + (not (eq coq-seq-process-require-current-buffer (current-buffer))))) -(defun coq-compile-save-some-buffers () +(defun coq-seq-compile-save-some-buffers () "Save buffers according to `coq-compile-auto-save'. -Uses the local variable coq-process-require-current-buffer to pass the +Uses the local variable coq-seq-process-require-current-buffer to pass the current buffer (which contains the Require command) to -`coq-compile-save-buffer-filter'." - (let ((coq-process-require-current-buffer (current-buffer)) +`coq-seq-compile-save-buffer-filter'." + (let ((coq-seq-process-require-current-buffer (current-buffer)) unconditionally buffer-filter) (cond ((eq coq-compile-auto-save 'ask-coq) (setq unconditionally nil - buffer-filter 'coq-compile-save-buffer-filter)) + buffer-filter 'coq-seq-compile-save-buffer-filter)) ((eq coq-compile-auto-save 'ask-all) (setq unconditionally nil buffer-filter nil)) ((eq coq-compile-auto-save 'save-coq) (setq unconditionally t - buffer-filter 'coq-compile-save-buffer-filter)) + buffer-filter 'coq-seq-compile-save-buffer-filter)) ((eq coq-compile-auto-save 'save-all) (setq unconditionally t buffer-filter nil))) (save-some-buffers unconditionally buffer-filter))) -(defun coq-preprocess-require-commands () +(defun coq-seq-preprocess-require-commands () "Coq function for `proof-shell-extend-queue-hook'. If `coq-compile-before-require' is non-nil, this function performs the compilation (if necessary) of the dependencies." (if coq-compile-before-require (let (;; coq-object-hash-symbol serves as a pointer to the - ;; coq-obj-hash (see coq-make-lib-up-to-date). The hash + ;; coq-obj-hash (see coq-seq-make-lib-up-to-date). The hash ;; will be initialized when needed and stored in the value ;; cell of coq-object-hash-symbol. The symbol is initialized ;; here to use one hash for all the requires that are added now. @@ -492,15 +495,15 @@ compilation (if necessary) of the dependencies." (span-add-delete-action span `(lambda () - (coq-unlock-all-ancestors-of-span ,span))) - (coq-compile-save-some-buffers) + (coq-seq-unlock-all-ancestors-of-span ,span))) + (coq-seq-compile-save-some-buffers) ;; now process all required modules (while (string-match coq-require-id-regexp string start) (setq start (match-end 0)) - (coq-check-module 'coq-object-hash-symbol span + (coq-seq-check-module 'coq-object-hash-symbol span (match-string 1 string)))))))))) -(add-hook 'proof-shell-extend-queue-hook 'coq-preprocess-require-commands) +(add-hook 'proof-shell-extend-queue-hook 'coq-seq-preprocess-require-commands) -- cgit v1.2.3