diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-05-20 12:59:20 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-05-20 12:59:20 +0000 |
| commit | ed2d995e2ecc9447b0f4d5767a051d4bafc3763d (patch) | |
| tree | 7980efe5176089542d060a60f7e7c729f9a0af22 /generic | |
| parent | af6f0debc693ac4e47c257d51061fada3dad1d28 (diff) | |
Buglet in proof-mark-buffer-atomic
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 80405518..161dadcc 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -700,7 +700,8 @@ to allow other files loaded by proof assistants to be marked read-only." ;; or even, could include parsing inside PG. (save-excursion (set-buffer buffer) - (if (< (proof-unprocessed-begin) (proof-script-end)) + (save-excursion ;; prevent point moving if user viewing file + (if (< (proof-unprocessed-begin) (proof-script-end)) (let ((span (make-span (proof-unprocessed-begin) (proof-script-end))) cmd) @@ -735,7 +736,7 @@ to allow other files loaded by proof assistants to be marked read-only." (proof-init-segmentation) (set-span-property span 'type 'comment)) ;; End of locked region is always end of buffer - (proof-set-locked-end (proof-script-end)))))) + (proof-set-locked-end (proof-script-end))))))) |