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. --- generic/proof-shell.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 6c0492aa..d9458eb8 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -88,9 +88,11 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.") (defsubst proof-shell-invoke-callback (listitem) "From `proof-action-list' LISTITEM, invoke the callback on the span." - (condition-case nil + (condition-case err (funcall (nth 2 listitem) (car listitem)) - (error nil))) + (error + (message "error escaping proof-shell-invoke-callback: %s" err) + nil))) (defvar proof-second-action-list-active nil "Signals that some items are waiting outside of `proof-action-list'. -- cgit v1.2.3 From 93a0d1ca16fd30e89e312932008106bc5503386f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 12 Dec 2016 10:05:00 +0100 Subject: fix generic interrupt procedure to interrupt parallel background compilation --- generic/proof-config.el | 7 ++++++- generic/proof-shell.el | 22 ++++++++++++++-------- 2 files changed, 20 insertions(+), 9 deletions(-) (limited to 'generic') diff --git a/generic/proof-config.el b/generic/proof-config.el index b4898a35..8ce53168 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier than `proof-shell-handle-error-or-interrupt-hook', which runs when the interrupt is acknowledged inside `proof-shell-exec-loop'. -This hook also runs when the proof assistent is killed." +This hook also runs when the proof assistent is killed. + +Hook functions should set the dynamic variable `prover-was-busy' +to t if there might have been a reason to interrupt. Otherwise +the generic interrupt handler might issue a prover-not-busy +error." :type '(repeat function) :group 'proof-shell) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7a397a06..51038fa6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -464,7 +464,9 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (proc (get-buffer-process (current-buffer))) (bufname (buffer-name))) (message "%s, cleaning up and exiting..." bufname) - (run-hooks 'proof-shell-signal-interrupt-hook) + (let (prover-was-busy) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook)) (redisplay t) (when (and alive proc) @@ -826,14 +828,18 @@ In the first case, PG will terminate the queue of commands at the first available point. In the second case, you may need to press enter inside the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)." (interactive) - (unless (proof-shell-live-buffer) + (let ((prover-was-busy nil)) + (unless (proof-shell-live-buffer) (error "Proof process not started!")) - (unless proof-shell-busy - (error "Proof process not active!")) - (setq proof-shell-interrupt-pending t) - (with-current-buffer proof-shell-buffer - (interrupt-process)) - (run-hooks 'proof-shell-signal-interrupt-hook)) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook) + (if proof-shell-busy + (progn + (setq proof-shell-interrupt-pending t) + (with-current-buffer proof-shell-buffer + (interrupt-process))) + (unless prover-was-busy + (error "Proof process not active!"))))) -- cgit v1.2.3 From 515026c1a268817075d37f748db303d05b0abb00 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 28 Dec 2016 13:04:26 +0100 Subject: fix prooftree crash with long evar lines --- generic/proof-tree.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'generic') diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 03af645e..77d3cc33 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -556,7 +556,8 @@ Runs on process status changes and cleans up when prooftree dies." "Start the external prooftree process. Does also initialize the communication channel and some internal variables." - (let ((old-proof-tree (get-process proof-tree-process-name))) + (let ((process-connection-type nil) ; use pipes, see emacs bug #24531 + (old-proof-tree (get-process proof-tree-process-name))) ;; reset output marker (when proof-tree-output-marker (set-marker proof-tree-output-marker nil) -- cgit v1.2.3