diff options
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 1f31c1d3..40e3a4d7 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -261,6 +261,16 @@ ensure-vo Ensure that all library dependencies are present as .vo (eq coq-compile-quick 'quick-no-vio2vo) (eq coq-compile-quick 'quick-and-vio2vo))) +(defcustom coq-compile-keep-going t + "Continue compilation after the first error as far as possible. +Similar to ``make -k'', with this option enabled, the background +compilation continues after the first error as far as possible. +With this option disabled, the background compilation is +immediately stopped after the first error.") + +;; define coq-compile-keep-going-toggle +(proof-deftoggle coq-compile-keep-going) + (defcustom coq-max-background-compilation-jobs 'all-cpus "Maximal number of parallel jobs, if parallel compilation is enabled. Use the number of available CPU cores if this is set to @@ -544,7 +554,10 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." (defun coq-unlock-ancestor (ancestor-src) "Unlock ANCESTOR-SRC." - (let* ((true-ancestor (file-truename ancestor-src))) + (let* ((default-directory + (buffer-local-value 'default-directory + (or proof-script-buffer (current-buffer)))) + (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))))) @@ -561,11 +574,14 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'. If needed, reinitialize `coq--compile-response-buffer'. Then display COMMAND and ERROR-MESSAGE." - (unless (buffer-live-p coq--compile-response-buffer) + (unless (buffer-live-p (get-buffer coq--compile-response-buffer)) (coq-init-compile-response-buffer)) - (let ((inhibit-read-only t)) + (let ((inhibit-read-only t) + (deactivate-mark nil)) (with-current-buffer coq--compile-response-buffer - (insert command "\n" error-message))) + (save-excursion + (goto-char (point-max)) + (insert command "\n" error-message "\n")))) (when display (coq-display-compile-response-buffer))) |