diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-08 02:04:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-08 02:04:19 +0000 |
| commit | 2ee1b4b96e50778b7f64951e20f0927c416d90f5 (patch) | |
| tree | 498d066cf8ab18df5ed8c755bd8e6156f6d5ee19 /generic | |
| parent | adfd2e8ef45c8d8881a25dfb30b00372ed46e74f (diff) | |
Robustness fixes/bug notes
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fcc0027e..f87f124d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -248,11 +248,11 @@ If END is at or before (point-min), remove the locked region. Otherwise set the locked region to be from (point-min) to END." (if (>= (point-min) end) (proof-detach-locked) - (set-span-endpoints proof-locked-span (point-min) end) - ;; FIXME: the next line doesn't fix the disappearing regions - ;; (was span property is lost in latest FSF Emacs, maybe?) - ;; (set-span-property proof-locked-span 'face 'proof-locked-face) - )) + (set-span-endpoints + proof-locked-span + (point-min) + (min (point-max) end) ;; safety: sometimes called with end>point-max(?) + ))) ;; Reimplemented this to mirror above because of remaining ;; span problen @@ -1181,7 +1181,10 @@ the ACS is marked in the current buffer. If CMD does not match any, (let ((end (span-end span)) cmd) ;; State of spans after advancing: (proof-set-locked-end end) - (proof-set-queue-start end) + ;; FIXME: bug here, can sometimes arrive with queue span already detached. + ;; (I think when complete file process is requested during scripting) + (if (span-live-p proof-queue-span) + (proof-set-queue-start end)) (setq cmd (span-property span 'cmd)) (cond ;; CASE 1: Comments just get highlighted |