diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 34 |
1 files changed, 25 insertions, 9 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 2c93d92d..cc53f3bb 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -235,8 +235,7 @@ Also clear list of script portions." (span-set-property proof-locked-span 'start-closed t) (span-set-property proof-locked-span 'end-open t) (proof-span-read-only proof-locked-span) - (if proof-colour-locked - (span-set-property proof-locked-span 'face 'proof-locked-face)) + (proof-colour-locked-span) (span-detach proof-locked-span) (setq proof-overlay-arrow (make-marker)) (setq overlay-arrow-position proof-overlay-arrow) @@ -246,13 +245,28 @@ Also clear list of script portions." ;;;###autoload (defun proof-colour-locked () - "Alter the colour of the locked region according to variable `proof-colour-locked'." + "Alter the colour of all locked regions according to variable `proof-colour-locked'." (interactive) (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script) (and (span-live-p proof-locked-span) - (if proof-colour-locked - (span-set-property proof-locked-span 'face 'proof-locked-face) - (span-set-property proof-locked-span 'face nil))))) + (proof-colour-locked-span)))) + +(defun proof-colour-locked-span () + "Alter the colour of the locked region according to variable `proof-colour-locked'." + (if proof-colour-locked + (span-set-property proof-locked-span 'face 'proof-locked-face) + (span-set-property proof-locked-span 'face nil))) + +(defun proof-sticky-errors () + "Alter the colour of sticky errors to match `proof-sticky-errors'. +This function is not yet implemented, so the colouring will stay +in effect until the regions are next cleared, or only be added the +next time an error is processed." + ;; TODO: we need to tag spans separately as error spans, and + ;; map over all spans in all buffers. + ) + + ;; ** Restarting and clearing spans @@ -308,9 +322,10 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." ;; jump to start of error: should this be configurable? (goto-char (span-start badspan)) (skip-chars-forward " \t\n")) - (pg-set-span-helphighlights badspan - 'proof-script-error-face - 'underline)) + (when proof-sticky-errors + (pg-set-span-helphighlights badspan + 'proof-script-highlight-error-face + 'proof-script-sticky-error-face))) (proof-script-delete-spans start end))) (defun proof-script-delete-spans (beg end) @@ -323,6 +338,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (span-delete-spans beg end 'pghelp)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |