- change to proof-restart-buffers for unlocking ancestors

- improve internal docs for unlocking

2 files changed, 11 insertions, 4 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 69e3c31e..ec1f05bf 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -275,9 +275,11 @@ next time an error is processed."
 
 (defun proof-restart-buffers (buffers)
   "Remove all extents in BUFFERS and maybe reset `proof-script-buffer'.
-No effect on a buffer which is nil or killed.  If one of the buffers
-is the current scripting buffer, then `proof-script-buffer'
-will deactivated."
+The high-level effect is that all members of BUFFERS are
+completely unlocked, including all the necessary cleanup. No
+effect on a buffer which is nil or killed. If one of the buffers
+is the current scripting buffer, then `proof-script-buffer' will
+deactivated."
   (mapcar
    (lambda (buffer)
      (save-excursion
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index c70c4eaa..be127b8a 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1151,7 +1151,12 @@ A subroutine of `proof-shell-process-urgent-message'."
       (proof-interrupt-process)))
 
 (defun proof-shell-process-urgent-message-retract (start end)
-  "A subroutine of `proof-shell-process-urgent-message'."
+  "A subroutine of `proof-shell-process-urgent-message'.
+Takes files off `proof-included-files-list' and calls
+`proof-restart-buffers' to do the necessary clean-up on those
+buffers visting a file that disappears from
+`proof-included-files-list'. So in some respect this function is
+inverse to `proof-register-possibly-new-processed-file'."
   (let ((current-included proof-included-files-list))
     (setq proof-included-files-list
 	  (funcall proof-shell-compute-new-files-list))