From 687e008bc80ca6f66ca8920296c2e8dab889c752 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 8 Dec 2016 16:06:17 +0100 Subject: option coq-compile-keep-going for parallel compilation With this option set, compilation continues after the first error to compile as much as possible and to potentially report more than one error. --- coq/coq-compile-common.el | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) (limited to 'coq/coq-compile-common.el') 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))) -- cgit v1.2.3