When killing process or scripting buffer, register file if it is complete, rather than always retracting.

2 files changed, 12 insertions, 7 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a527ed3d..e9ca77fc 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -810,6 +810,13 @@ an error is signalled here."
 		(and (eq action 'process) (proof-locked-region-full-p))
 		(error "%s of %s failed!" name buf)))))))
 
+(defun proof-deactivate-scripting-auto () 
+  "Deactivate scripting without asking questions.
+If the locked region is full, register the file as processed.
+Otherwise retract it."
+  (proof-deactivate-scripting
+   (proof-with-script-buffer
+    (if (proof-locked-region-full-p) 'process 'retract))))
 
 (defun proof-deactivate-scripting (&optional forcedaction)
   "Deactivate scripting for the active scripting buffer.
@@ -2357,13 +2364,13 @@ to restore them using `after-set-visited-file-name-hooks'."
 (defun proof-script-kill-buffer-fn ()
   "Value of kill-buffer-hook for proof script buffers.
 Clean up before a script buffer is killed.
-If killing the active scripting buffer, run proof-deactivate-scripting.
+If killing the active scripting buffer, run proof-deactivate-scripting-auto.
 Otherwise just do proof-restart-buffers to delete some spans from memory."
   ;; Deactivate scripting in the current buffer if need be, forcing
   ;; automatic retraction if the buffer is not fully processed.
   (unwind-protect
       (if (eq (current-buffer) proof-script-buffer)
-	  (proof-deactivate-scripting 'retract))
+	  (proof-deactivate-scripting-auto))
     (proof-restart-buffers (list (current-buffer)))
     ;; Hide away goals, response, and tracing.  This is a hack because
     ;; otherwise we can lead the user to frustration with the
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3242a8a6..6dd9602f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -338,11 +338,9 @@ exited by hand (or exits by itself)."
 	      ;; 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)
+	      ;; partly processed when exiting, and registering completed
+	      ;; files).  
+	      (proof-deactivate-scripting-auto)
 	      ;; 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.