- 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

1 files changed, 11 insertions, 0 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index b637c568..280b98cf 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1633,6 +1633,17 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'."
   :type '(repeat function)
   :group 'proof-shell)
 
+(defcustom proof-shell-signal-interrupt-hook nil
+  "Run when the user tries to interrupt the prover.
+This hook is run inside `proof-interrupt-process' when the user
+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."
+  :type '(repeat function)
+  :group 'proof-shell)
+
 (defcustom proof-shell-pre-interrupt-hook
   nil
   "Run immediately after `comint-interrupt-subjob' is called.