From 5b3f191a9b989bd68bee27ce84aeeeb9fa1060fd Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Mon, 14 Mar 2011 09:29:48 +0000
Subject: - change to proof-restart-buffers for unlocking ancestors - improve
 internal docs for unlocking

---
 generic/proof-script.el | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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

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
-- 
cgit v1.2.3