From 81bc37ba8e26df936d3a09e02e6ed70f8b8804a8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 15 Jan 2002 15:05:15 +0000
Subject: Inspect quit-flag when displaying tracing output; send an interrupt
 to the prover if set.

---
 generic/proof-shell.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f527eb10..3ace83ed 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1487,7 +1487,11 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
       ;; fully-occupied processing prover output
       (and (fboundp 'redisplay-frame)
 	   ;; XEmacs fn 
-	   (redisplay-frame)))
+	   (redisplay-frame))
+      ;; If user quits during tracing output, send an interrupt
+      ;; to the prover.
+      (if (and quit-flag proof-action-list)
+	  (proof-interrupt-process)))
 	   
       ;; Similarly, try to determine if there are command events
       ;; waiting which are being ignored;
-- 
cgit v1.2.3