[ 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.

Reply via email to