Hi,
I looked around, but I could not find the inverse of
proof-register-possibly-new-processed-file. This inverse should
delete a file from proof-included-files-list and unlock its
buffer, if it exists.
There is proof-unregister-buffer-file-name, but
- it only works on buffers
- it does not unlock the buffer
I also looked at proof-retract-buffer, but it wants to change the
active scripting buffer, which is not the right thing to do when
unlocking an ancestor.
I finally came up with the following
(defun coq-unlock-ancestor (ancestor-src)
"Unlock ANCESTOR-SRC."
(let* ((true-ancestor (file-truename ancestor-src))
(buffer (find-buffer-visiting true-ancestor)))
(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))))))
This works in my tests, but I am not sure, if it is the right
thing.
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
