diff options
| -rw-r--r-- | coq/coq-compile-common.el | 42 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 40 |
2 files changed, 43 insertions, 39 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 4e2e7802..1e10f0dd 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -448,6 +448,48 @@ the command whose output will appear in the buffer." (proof-resize-window-tofit window)))))) +;; save some buffers + +(defvar coq-compile-buffer-with-current-require + "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'.") + +(defun coq-compile-save-buffer-filter () + "Filter predicate for `coq-compile-save-some-buffers'. +See also `save-some-buffers'. Returns t for buffers with major +mode 'coq-mode' different from +`coq-compile-buffer-with-current-require' and nil for all other +buffers. The buffer to test must be current." + (and + (eq major-mode 'coq-mode) + (not (eq coq-compile-buffer-with-current-require + (current-buffer))))) + +(defun coq-compile-save-some-buffers () + "Save buffers according to `coq-compile-auto-save'. +Uses the local variable coq-compile-buffer-with-current-require to pass the +current buffer (which contains the Require command) to +`coq-compile-save-buffer-filter'." + (let ((coq-compile-buffer-with-current-require (current-buffer)) + unconditionally buffer-filter) + (cond + ((eq coq-compile-auto-save 'ask-coq) + (setq unconditionally nil + buffer-filter 'coq-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)) + ((eq coq-compile-auto-save 'save-all) + (setq unconditionally t + buffer-filter nil))) + (save-some-buffers unconditionally buffer-filter))) + + ;; kill coqtop on script buffer change (defun coq-switch-buffer-kill-proof-shell () 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)) |