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.

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)))