aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2011-03-14 09:29:48 +0000
committerGravatar Hendrik Tews <hendrik@askra.de>2011-03-14 09:29:48 +0000
commit5b3f191a9b989bd68bee27ce84aeeeb9fa1060fd (patch)
tree3b966cb4659b485bead02403739fc9560174cd72
parentdfb79401d8ea75588305c6e9789895c9c646e76b (diff)
- change to proof-restart-buffers for unlocking ancestors
- improve internal docs for unlocking
-rw-r--r--coq/coq.el9
-rw-r--r--doc/PG-adapting.texi36
-rw-r--r--generic/proof-script.el8
-rw-r--r--generic/proof-shell.el7
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))