Merge remote-tracking branch 'OFFICIAL/master'

3 files changed, 26 insertions, 12 deletions

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 4cb46b0c..51038fa6 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'.
@@ -462,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)
@@ -824,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!")))))
 
 
 
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)