From 49fda3fd12b9985da15a52756e4a18fd2bc5ba2b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 19 Jul 2002 10:38:48 +0000
Subject: Variable name change proof-comment-{start,end}-regexp ->
 proof-script-comment-{start,end}-regexp.

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

(limited to 'generic/proof-shell.el')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 2cea0c4c..e171da86 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -375,7 +375,7 @@ exited by hand (or exits by itself)."
     (message "%s, cleaning up and exiting..." bufname)
     (let ((inhibit-quit t)		; disable C-g for now
 	  timeout-id)
-      (sit-for 0)			; redisplay
+      (sit-for 0)			; redisplay [does it work?]
       (if alive				; process still there
 	  (progn
 	    (catch 'exited
@@ -387,6 +387,10 @@ exited by hand (or exits by itself)."
 	      ;; partly processed when exiting, and registering completed
 	      ;; files).  
 	      (proof-deactivate-scripting-auto)
+	      ;; FIXME: if the shell is busy now, we should wait
+	      ;; for a while (in case deactivate causes processing)
+	      ;; and the send an interrupt.
+
 	      ;; Second, we try to shut down the proof process
 	      ;; politely.  Do this before deleting other buffers,
 	      ;; etc, so that any closing down processing works okay.
-- 
cgit v1.2.3