diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2012-11-13 22:05:11 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2012-11-13 22:05:11 +0000 |
| commit | 2243cc9d87d4993ca6b0281f7171b883dd9fd52d (patch) | |
| tree | 10b5d50bc8003df6a6d7f90973ecd60f779649c7 /coq/coq-seq-compile.el | |
| parent | 06b2407614a9f81795e47d2710826d0973edbaf1 (diff) | |
- first version of parallel asynchronous compilation for coq in
coq-par-compile.el (must be activated via
coq-compile-parallel-in-background)
- items in the queue region are not necessarily in
proof-action-list any more! Require commands and the following
items are stored elsewhere until the compilation finishes.
Variable proof-second-action-list-active notifies the generic
machinery if queue items are stored elsewhere. In this case,
Proof General must neither release the proof shell lock nor
delete the queue span when proof-action-list is empty.
- to kill background processes as early as possible, the new hook
proof-shell-signal-interrupt-hook is used
Diffstat (limited to 'coq/coq-seq-compile.el')
| -rw-r--r-- | coq/coq-seq-compile.el | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index f9543886..e7579f81 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -21,6 +21,7 @@ (eval-when (compile) (defvar queueitems nil) ; dynamic scope in p-s-extend-queue-hook (defvar coq-compile-before-require nil) ; defpacustom + (defvar coq-compile-parallel-in-background nil) ; defpacustom (defvar coq-confirm-external-compilation nil)); defpacustom (require 'coq-compile-common) @@ -390,10 +391,6 @@ compilation (if necessary) of the dependencies." (coq-seq-check-module 'coq-object-hash-symbol span (match-string 1 string)))))))))) -(add-hook 'proof-shell-extend-queue-hook 'coq-seq-preprocess-require-commands) - - - (provide 'coq-seq-compile) |