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

---
 coq/coq.el | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 6c59bda7..2c048ad5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1210,15 +1210,10 @@ properly unlock ANCESTOR-SRC on retract."
 
 (defun coq-unlock-ancestor (ancestor-src)
   "Unlock ANCESTOR-SRC."
-  (let* ((true-ancestor (file-truename ancestor-src))
-         (buffer (find-buffer-visiting true-ancestor)))
-    ;(message "unlock %s in buf %s" ancestor-src buffer)
+  (let* ((true-ancestor (file-truename ancestor-src)))
     (setq proof-included-files-list
           (delete true-ancestor proof-included-files-list))
-    (if buffer
-        (with-current-buffer buffer
-          (proof-set-locked-end (point-min))
-          (proof-script-delete-spans (point-min) (point-max))))))
+    (proof-restart-buffers (proof-files-to-buffers (list true-ancestor)))))
 
 (defun coq-unlock-all-ancestors-of-span (span)
   "Unlock all ancestors that have been locked when SPAN was asserted."
-- 
cgit v1.2.3