[ Hendrik - you asked me to follow up on this, below is the message I
sent before to you 25/1, not sent to the list. ]
When this is driven by messages from the prover, this function in
proof-shell.el does the job:
proof-shell-process-urgent-message-retract
It uses proof-restart-buffers which you might want to reuse, does a bit
more cleanup than your version.
- D.
On 25/01/11 14:47, Hendrik Tews wrote:
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
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
