From f953b34552f06fa7e1cac60494373be67e44ddf8 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 5 Nov 2012 13:18:08 +0000 Subject: move buffer saving to coq-compile-common --- coq/coq-seq-compile.el | 40 +--------------------------------------- 1 file changed, 1 insertion(+), 39 deletions(-) (limited to 'coq/coq-seq-compile.el') diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 2dd1e954..27521c04 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -371,44 +371,6 @@ queue." (coq-seq-make-lib-up-to-date (symbol-value coq-object-local-hash-symbol) span module-obj-file))))) -(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-seq-compile-save-some-buffers' to -`coq-seq-compile-save-buffer-filter'.") - -(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-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-seq-process-require-current-buffer - (current-buffer))))) - -(defun coq-seq-compile-save-some-buffers () - "Save buffers according to `coq-compile-auto-save'. -Uses the local variable coq-seq-process-require-current-buffer to pass the -current buffer (which contains the Require command) to -`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-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-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-seq-preprocess-require-commands () "Coq function for `proof-shell-extend-queue-hook'. If `coq-compile-before-require' is non-nil, this function performs the @@ -431,7 +393,7 @@ compilation (if necessary) of the dependencies." span `(lambda () (coq-seq-unlock-all-ancestors-of-span ,span))) - (coq-seq-compile-save-some-buffers) + (coq-compile-save-some-buffers) ;; now process all required modules (while (string-match coq-require-id-regexp string start) (setq start (match-end 0)) -- cgit v1.2.3