diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2013-01-03 09:33:38 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2013-01-03 09:33:38 +0000 |
| commit | 28a0ffbcb1c6a442a4f5d4a3825ea303dca8b854 (patch) | |
| tree | 745cd4df971687f6a8843c9658f4d00f65ab8de1 | |
| parent | b35facae2146b09570c0636ed92e82af641db6b6 (diff) | |
- fix asserting when parallel background compilation is in progress
- fix aborting background compilation on error
| -rw-r--r-- | coq/coq-compile-common.el | 4 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 4 | ||||
| -rw-r--r-- | generic/proof-shell.el | 3 |
3 files changed, 11 insertions, 0 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index e24cc5b2..a66f68c8 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -63,6 +63,8 @@ Must be used together with `coq-seq-disable'." (add-hook 'proof-shell-extend-queue-hook 'coq-par-preprocess-require-commands) (add-hook 'proof-shell-signal-interrupt-hook + 'coq-par-emergency-cleanup) + (add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-par-emergency-cleanup)) (defun coq-par-disable () @@ -71,6 +73,8 @@ Must be used together with `coq-seq-enable'." (remove-hook 'proof-shell-extend-queue-hook 'coq-par-preprocess-require-commands) (remove-hook 'proof-shell-signal-interrupt-hook + 'coq-par-emergency-cleanup) + (remove-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-par-emergency-cleanup)) (defun coq-seq-enable () diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index c7d52761..8e8c7772 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -1166,6 +1166,9 @@ Finally, `proof-second-action-list-active' is set if I keep some queue items because they have to wait for a compilation job. Then the maximal number of background compilation jobs is started." (when coq-compile-before-require + (when coq-debug-auto-compilation + (message "%d items were added to the queue, scan for require" + (length queueitems))) (unless coq-last-compilation-job (coq-par-init-compilation-hash) (coq-par-init-ancestor-hash)) @@ -1177,6 +1180,7 @@ the maximal number of background compilation jobs is started." (put coq-last-compilation-job 'queueitems (nconc (get coq-last-compilation-job 'queueitems) (car splitted-items))) + (setq queueitems nil) (message "attach first %s items to job %s" (length (car splitted-items)) (get coq-last-compilation-job 'name))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 3c73c53d..6bfbef51 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -681,6 +681,9 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')." (save-excursion (proof-script-clear-queue-spans-on-error badspan (eq err-or-int 'interrupt)))) + ;; Note: coq-par-emergency-cleanup, which might be called via + ;; proof-shell-handle-error-or-interrupt-hook below, assumes that + ;; proof-action-list is empty on error. (setq proof-action-list nil) (proof-release-lock) (unless flags |