diff options
| author | David Aspinall | 1999-11-08 18:03:12 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-08 18:03:12 +0000 |
| commit | 65001bfa7d7ebef886755e00ef476c19d9370515 (patch) | |
| tree | 0fb9548f3d1fcda3e2f4bd11f68747715ac56931 /generic/proof.el | |
| parent | a90f26e3eb52582e4c3107b83ff00b6abaf8054e (diff) | |
Docstring for proof-included-files.
Diffstat (limited to 'generic/proof.el')
| -rw-r--r-- | generic/proof.el | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/generic/proof.el b/generic/proof.el index c9ed9a1a..2f43540f 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -101,14 +101,15 @@ This list contains files in canonical truename format Whenever a new file is being processed, it gets added to this list via the proof-shell-process-file configuration settings. -When the prover retracts across file boundaries, this list -is resynchronised via the proof-shell-retract-files-regexp and -proof-shell-compute-new-files-list configuration settings. +When the prover retracts a file, this list is resynchronised via the +proof-shell-retract-files-regexp and proof-shell-compute-new-files-list +configuration settings. Only files which have been *fully* processed should be included here. -Proof General itself will automatically add the filenames of script -buffers which are completely read, when scripting is deactivated or -switched to another buffer. +Proof General itself will automatically add the filenames of a script +buffer which has been completely read when scripting is deactivated. +It will automatically remove the filename of a script buffer which +is completely unread when scripting is deactivated. NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant |