fix generic interrupt procedure to interrupt parallel background compilation

5 files changed, 64 insertions, 30 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index ec8d5e80..87f61df6 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -203,7 +203,12 @@ It was constructed with `proof-defstringset-fn'.")
       :selected coq-confirm-external-compilation
       :active (and coq-compile-before-require
 		   (not (equal coq-compile-command "")))
-      :help "Confirm external compilation command, see `coq-compile-command'."])
+      :help "Confirm external compilation command, see `coq-compile-command'."]
+     ["Abort Background Compilation"
+      coq-par-emergency-cleanup
+      :active (and coq-compile-before-require
+		   coq-compile-parallel-in-background)
+      :help "Abort background compilation and kill all compilation processes."])
     ""
     ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"]
     ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"]
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index d5b84d46..efbb2d3c 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -717,7 +717,8 @@ function returns () if MODULE-ID comes from the standard library."
 ;;; manage background jobs
 
 (defun coq-par-kill-all-processes ()
-  "Kill all background coqc, coqdep or vio2vo compilation processes."
+  "Kill all background coqc, coqdep or vio2vo compilation processes.
+Return t if some process was killed."
   ;; need to first mark processes as killed, because delete process
   ;; starts running sentinels in the order processes terminated, so
   ;; after the first delete-process we see sentinentels of non-killed
@@ -741,7 +742,8 @@ function returns () if MODULE-ID comes from the standard library."
 		    (get (process-get process 'coq-compilation-job) 'name)
 		    (process-name process)))))
      (process-list))
-    (setq coq--current-background-jobs 0)))
+    (setq coq--current-background-jobs 0)
+    kill-needed))
 
 (defun coq-par-unlock-all-ancestors-on-error ()
   "Unlock ancestors which are not in an asserted span.
@@ -758,22 +760,29 @@ Used for unlocking ancestors on compilation errors."
   "Emergency cleanup for parallel background compilation.
 Kills all processes, unlocks ancestors, clears the queue region
 and resets the internal state."
-  (when coq--debug-auto-compilation
-    (message "emergency cleanup"))
-  (coq-par-kill-all-processes)
-  (setq coq-par-compilation-queue (coq-par-new-queue))
-  (setq coq--last-compilation-job nil)
-  (setq coq-par-vio2vo-queue (coq-par-new-queue))
-  (setq coq--compile-vio2vo-in-progress nil)
-  (when coq--compile-vio2vo-delay-timer
-    (cancel-timer coq--compile-vio2vo-delay-timer))
-  (when proof-action-list
-    (setq proof-shell-interrupt-pending t))
-  (coq-par-unlock-all-ancestors-on-error)
-  (proof-release-lock)
-  (proof-detach-queue)
-  (setq proof-second-action-list-active nil)
-  (coq-par-init-compilation-hash))
+  (interactive)				; needed for menu
+  (let (proc-killed was-busy)
+    (when coq--debug-auto-compilation
+      (message "emergency cleanup"))
+    (setq proc-killed (coq-par-kill-all-processes))
+    (when (and (boundp 'prover-was-busy)
+	       (or proc-killed coq--last-compilation-job
+		   coq--compile-vio2vo-in-progress
+		   coq--compile-vio2vo-delay-timer))
+      (setq prover-was-busy t))
+    (setq coq-par-compilation-queue (coq-par-new-queue))
+    (setq coq--last-compilation-job nil)
+    (setq coq-par-vio2vo-queue (coq-par-new-queue))
+    (setq coq--compile-vio2vo-in-progress nil)
+    (when coq--compile-vio2vo-delay-timer
+      (cancel-timer coq--compile-vio2vo-delay-timer))
+    (coq-par-unlock-all-ancestors-on-error)
+    (when proof-action-list
+      (setq proof-shell-interrupt-pending t))
+    (proof-release-lock)
+    (proof-detach-queue)
+    (setq proof-second-action-list-active nil)
+    (coq-par-init-compilation-hash)))
 
 (defun coq-par-process-filter (process output)
   "Store output from coq background compilation."
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 31594b9d..be29a660 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4515,6 +4515,12 @@ the number of parallel background jobs and set
 error.
 @end itemize
 
+To abort parallel background compilation, use @code{C-c C-c}
+(@code{proof-interrupt-process}), the tool bar interrupt icon,
+the menu entry @code{Abort Background Compilation} (menu
+@code{Coq -> Auto Compilation}) or kill the Coq toplevel via
+@code{C-c C-x} (@code{proof-shell-exit}). To abort synchronous
+single threaded compilation, simply hit @code{C-g}.
 
 
 @menu
@@ -4599,8 +4605,11 @@ runs up to @code{coq-max-background-compilation-jobs} coqdep and
 coqc jobs in parallel in asynchronous subprocesses (or uses all
 your CPU cores if @code{coq-max-background-compilation-jobs}
 equals @code{'all-cpus}). Your Emacs will stay responsive during
-compilation. Use @code{C-c C-c} or the tool bar icons for
-interrupt or restart to interrupt compilation.
+compilation. To abort the background compilation process, use
+@code{C-c C-c} (@code{proof-interrupt-process}), the tool bar
+interrupt icon, the menu entry @code{Abort Background
+Compilation} (menu @code{Coq -> Auto Compilation}) or kill the
+Coq toplevel via @code{C-c C-x} (@code{proof-shell-exit}).
 
 For the usual case, you have at most
 `coq-max-background-compilation-jobs' parallel processes
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!")))))