Fixes for FSF Emacs handling of processes, kill buffer hooks,

and live/dead overlays.

4 files changed, 71 insertions, 47 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index d9d5c686..13a441c4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1018,18 +1018,19 @@ a space or newline will be inserted automatically."
 
 
 (defun proof-done-retracting (span)
-  "Updates display after proof process has reset its state. See also
-the documentation for `proof-retract-until-point'. It optionally
-deletes the region corresponding to the proof sequence."
-  (let ((start (span-start span))
-        (end (span-end span))
-	(kill (span-property span 'delete-me)))
-    (unless (proof-locked-region-empty-p)
-      (proof-set-locked-end start)
-      (proof-set-queue-end start))
-    (delete-spans start end 'type)
-    (delete-span span)
-    (if kill (kill-region start end))))
+  "Update display after proof process has reset its state.
+See also the documentation for `proof-retract-until-point'.
+Optionally delete the region corresponding to the proof sequence."
+  (if (span-live-p span)
+      (let ((start (span-start span))
+	    (end (span-end span))
+	    (kill (span-property span 'delete-me)))
+	(unless (proof-locked-region-empty-p)
+	  (proof-set-locked-end start)
+	  (proof-set-queue-end start))
+	(delete-spans start end 'type)
+	(delete-span span)
+	(if kill (kill-region start end)))))
 
 (defun proof-setup-retract-action (start end proof-command delete-region)
   (let ((span (make-span start end)))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 83098f88..1a978acb 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -303,45 +303,56 @@ of the queue region."
 
 (defun proof-shell-kill-function ()
   "Function run when a proof-shell buffer is killed.
-Value for kill-buffer-hook in shell buffer.
 Attempt to shut down the proof process nicely and
-clears up all the locked regions and state variables."
+clear up all the locked regions and state variables.
+Value for kill-buffer-hook in shell buffer.
+Also called by proof-shell-bail-out if the process is
+exited by hand (or exits by itself)."
   (let* ((alive    (comint-check-proc (current-buffer)))
-	 (proc      (get-buffer-process (current-buffer)))
-	 (bufname   (buffer-name)))
+	 (proc     (get-buffer-process (current-buffer)))
+	 (bufname  (buffer-name)))
     (message "%s, cleaning up and exiting..." bufname)
-    (sit-for 0)				; redisplay
-    (if alive				; process still there
-	(progn
-	  ;; Try to shut it down politely
-	  ;; Do this before deleting other buffers, etc, so that
-	  ;; any closing down processing works okay.
-	  (if proof-shell-quit-cmd
-	      (comint-send-string proc
-				  (concat proof-shell-quit-cmd "\n"))
-	    (comint-send-eof))
-	  ;; Wait a while for it to die before killing
-	  ;; it off more rudely.
-	  (set-process-sentinel proc
-				(lambda (p m) (throw 'exited t)))
+    (let ((inhibit-quit t))		; disable C-g for now
+      (sit-for 0)				; redisplay
+      (if alive				; process still there
 	  (catch 'exited
-	    (accept-process-output nil 10)
-	    (kill-process proc)
-	    ;; another chance to catch
-	    (accept-process-output))))
-    ;; Restart all scripting buffers
-    (proof-script-remove-all-spans-and-deactivate)
-    ;; Clear state
-    (setq proof-included-files-list nil
-	  proof-shell-busy nil
-	  proof-shell-proof-completed nil)
-    ;; Kill buffers associated with shell buffer
-    (if (buffer-live-p proof-goals-buffer)
-	(kill-buffer proof-goals-buffer))
-    (if (buffer-live-p proof-response-buffer)
-	(kill-buffer proof-response-buffer))
-    (message "%s exited." bufname)))
-
+	    (set-process-sentinel proc
+				  (lambda (p m) (throw 'exited t)))
+	    ;; Try to shut it down politely
+	    ;; Do this before deleting other buffers, etc, so that
+	    ;; any closing down processing works okay.
+	    (if proof-shell-quit-cmd
+		(comint-send-string proc
+				    (concat proof-shell-quit-cmd "\n"))
+	      (comint-send-eof))
+	    ;; Wait a while for it to die before killing
+	    ;; it off more rudely.  In XEmacs, accept-process-output
+	    ;; or sit-for will run process sentinels if a process
+	    ;; changes state.
+	    ;; In FSF I've no idea how to get the process sentinel
+	    ;; to run outside the top-level loop.
+	    ;; So put an ugly timeout and busy wait here instead
+	    ;; of simply (accept-process-output nil 10).
+	    (add-timeout 10 (lambda (&rest args)
+			      (unless (comint-check-proc (current-buffer))
+				(kill-process proc))
+			      (throw 'exited t)) nil)
+	    (while (comint-check-proc (current-buffer))
+	      (sit-for 1))))
+      ;; For FSF Emacs, proc may be nil if killed already.
+      (if proc (set-process-sentinel proc nil))
+      ;; Restart all scripting buffers
+      (proof-script-remove-all-spans-and-deactivate)
+      ;; Clear state
+      (setq proof-included-files-list nil
+	    proof-shell-busy nil
+	    proof-shell-proof-completed nil)
+      ;; Kill buffers associated with shell buffer
+      (if (buffer-live-p proof-goals-buffer)
+	  (kill-buffer proof-goals-buffer))
+      (if (buffer-live-p proof-response-buffer)
+	  (kill-buffer proof-response-buffer))
+      (message "%s exited." bufname))))
 
 (defun proof-shell-exit ()
   "Query the user and exit the proof process.
diff --git a/generic/span-extent.el b/generic/span-extent.el
index fcc82258..597d262a 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -90,4 +90,10 @@ A span is before PT if it covers the character before PT."
   "Return span after SPAN with property PROP."
   (extent-at (extent-end-position span) nil prop nil 'after))
 
+(defsubst span-live-p (span)
+    "Return non-nil if SPAN is in a live buffer."
+  (and span
+       (extent-live-p span)
+       (buffer-live-p (extent-object span))))
+
 (provide 'span-extent)
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 6cb572df..8289bf3d 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -273,4 +273,10 @@ If there are two spans overlapping then this won't work."
     (if l (car l) nil)))
 
 
+(defsubst span-live-p (span)
+  "Return non-nil if SPAN is in a live buffer."
+  (and span
+       (overlay-buffer span)
+       (buffer-live-p (overlay-buffer span))))
+
 (provide 'span-overlay)