diff options
| author | David Aspinall | 1999-10-20 16:12:58 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-20 16:12:58 +0000 |
| commit | 251990ee91b756498025c0a75b96856475ea27bc (patch) | |
| tree | bd4b728ca7f3e4ae32d936fc5c70b5abf32bfdf9 /generic/proof-script.el | |
| parent | 6ed9aea8d30a2eabe4d7b52c5e1cb096fe792ad2 (diff) | |
Comments in proof-complete-buffer-atomic.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 694262fc..4bbb7d25 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -368,6 +368,15 @@ buffer is closed off atomically. This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only." +;; FIXME: this isn't quite right, because not all of the structure +;; in the locked region will be preserved when processing across several +;; files. +;; In particular, the span for a currently open goal should be removed. +;; Keeping the structure is an approximation to make up for the fact +;; that that no structure is created by loading files via the +;; proof assistant. +;; Future idea: proof assistant could ask Proof General to do the +;; loading, to alleviate file handling there?! (save-excursion (set-buffer buffer) (if (< (proof-unprocessed-begin) (proof-script-end)) |