From 189395ce88ba2d3208726ff7ccd007df57aa1524 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 30 Jun 2002 14:43:27 +0000
Subject: proof-shell-kill-function: deactivate scripting before shutting down
 prover

---
 generic/proof-shell.el | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 383bd69e..3242a8a6 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -335,9 +335,17 @@ exited by hand (or exits by itself)."
 	    (catch 'exited
 	      (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.
+	      ;; First, turn off scripting in any active scripting
+	      ;; buffer.  (This helps support persistent sessions with
+	      ;; Isabelle, for example, by making sure that no file is
+	      ;; partly processed when exiting).  Rather than
+	      ;; questioning the user, we behave as killing a script
+	      ;; buffer: forcibly retract a partly processed file and
+	      ;; always succeed.
+	      (proof-deactivate-scripting 'forceretract)
+	      ;; 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.
 	      (if proof-shell-quit-cmd
 		  (comint-send-string proc
 				      (concat proof-shell-quit-cmd "\n"))
-- 
cgit v1.2.3