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 ++------- doc/PG-adapting.texi | 36 ++++++++++++++++++++++++++++++------ generic/proof-script.el | 8 +++++--- generic/proof-shell.el | 7 ++++++- 4 files changed, 43 insertions(+), 17 deletions(-) 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." diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 297b9641..d122cad1 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2185,8 +2185,11 @@ read. @end defvar The way that @code{proof-included-files-list} is maintained is the key -to multiple file management. (But you should not set this variable -directly, it is managed via the configuration settings). +to multiple file management. Ideally you should not set this +variable directly, but instead use (some of) the various +configuration settings that enable functionality inside Proof +General for managing @code{proof-included-files-list} (see below +if the configuration setting do not suffice). @vindex proof-shell-process-file @vindex proof-shell-retract-files-regexp @@ -2288,6 +2291,20 @@ files, set @code{proof-cannot-reopen-processed-files} to @code{t}. for a automatic approximation to multiple file handling. @xref{Proof Script Settings}. +Internally Proof General uses +@code{proof-register-possibly-new-processed-file} to add a file +to @code{proof-included-files-list} and to possibly inform the +prover about this fact, @xref{Proof script mode}. The function +@code{proof-shell-process-urgent-message-retract} is responsible +for taking (possibly several) files off +@code{proof-included-files-list}. It relies on +@code{proof-shell-compute-new-files-list} (@pxref{Settings for +matching urgent messages from proof process}) to compute the new +value of @code{proof-included-files-list} and then calls +@code{proof-restart-buffers} on all those buffers that have been +taken off from @code{proof-included-files-list}, @xref{Proof +script mode}. + @node Configuring Editing Syntax @chapter Configuring Editing Syntax @@ -3088,6 +3105,10 @@ A warning message is issued if the register request came from the proof assistant and Emacs has a modified buffer visiting the file. @end defun +(Unlocking is done by +@code{proof-shell-process-urgent-message-retract} together with +@code{proof-restart-buffers}.) + An important pair of functions activate and deactivate scripting for the current buffer. A change in the state of active scripting can trigger various actions, such as starting up the proof assistant, or altering @@ -3251,7 +3272,8 @@ user hasn't saved the latest edits. Therefore it is right to query saves here. @end defun -To clean up when scripting is stopped, a script buffer is killed, or the +To clean up when scripting is stopped, a script buffer is killed, +a file is retract (and thus must be unlocked), or the proof assistant exits, we use the functions @code{proof-restart-buffers} and @code{proof-script-remove-all-spans-and-deactivate}. @@ -3259,9 +3281,11 @@ proof assistant exits, we use the functions @c TEXI DOCSTRING MAGIC: proof-restart-buffers @defun proof-restart-buffers buffers Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@* -No effect on a buffer which is nil or killed. If one of the buffers -is the current scripting buffer, then @samp{@code{proof-script-buffer}} -will deactivated. +The high-level effect is that all members of @var{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 @samp{@code{proof-script-buffer}} will +deactivated. @end defun @c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate 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 diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c70c4eaa..be127b8a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1151,7 +1151,12 @@ A subroutine of `proof-shell-process-urgent-message'." (proof-interrupt-process))) (defun proof-shell-process-urgent-message-retract (start end) - "A subroutine of `proof-shell-process-urgent-message'." + "A subroutine of `proof-shell-process-urgent-message'. +Takes files off `proof-included-files-list' and calls +`proof-restart-buffers' to do the necessary clean-up on those +buffers visting a file that disappears from +`proof-included-files-list'. So in some respect this function is +inverse to `proof-register-possibly-new-processed-file'." (let ((current-included proof-included-files-list)) (setq proof-included-files-list (funcall proof-shell-compute-new-files-list)) -- cgit v1.2.3