diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 5e2f09ef..51847029 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -2333,7 +2333,6 @@ The key @kbd{C-c C-u} (@code{isa-retract-thy-file}) will retract (unlock) the theory file being edited. This unlocks the file and all its children (theory and ML files); no changes occur in Isabelle itself. - @c TEXI DOCSTRING MAGIC: isa-process-thy-file @deffn Command isa-process-thy-file file Process the theory file @var{file}. If interactive, use @code{buffer-file-name}. @@ -2341,7 +2340,11 @@ Process the theory file @var{file}. If interactive, use @code{buffer-file-name} @c TEXI DOCSTRING MAGIC: isa-retract-thy-file @deffn Command isa-retract-thy-file file -Retract the theory file @var{file}. If interactive, use @code{buffer-file-name}. +Retract the theory file @var{file}. If interactive, use @code{buffer-file-name}.@* +To prevent inconsistencies, scripting is deactivated before doing this. +So if scripting is active in an ML file which is not completely processed, +you will be asked to retract the file or process the remainder of it. +(If you process the rest of it it may subsequently be unlocked anyway). @end deffn @@ -3395,9 +3398,9 @@ buffer, so the regions are made empty by this function. For locking files loaded by a proof assistant, we use the next function. -@c TEXI DOCSTRING MAGIC: proof-mark-buffer-atomic -@defun proof-mark-buffer-atomic buffer -Mark @var{buffer} as having been processed in a single step. +@c TEXI DOCSTRING MAGIC: proof-complete-buffer-atomic +@defun proof-complete-buffer-atomic buffer +Make sure @var{buffer} is marked as completely processed, completing with a single step. If buffer already contains a locked region, only the remainder of the buffer is closed off atomically. |