diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 12:17:41 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 12:17:41 +0000 |
| commit | 9fa7615622788041afd81ec9bfd4772a036d67ab (patch) | |
| tree | 02127b7bcc28c8b0b46e14384857a574757e7df6 /generic/proof-depends.el | |
| parent | 60a84ffa180c02e7d78fadada20b58a238319bbf (diff) | |
Fix dep highlighting for Emacs 21 by setting priorities.
Diffstat (limited to 'generic/proof-depends.el')
| -rw-r--r-- | generic/proof-depends.el | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 22faaa83..af83afe9 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -174,11 +174,15 @@ If LIST is empty, return a disabled menu item with NAME." (if proof-shell-show-dependency-cmd ;; robustness (proof-shell-invisible-command (format proof-shell-show-dependency-cmd thm)))) +(defconst pg-dep-span-priority 500) +(defconst pg-ordinary-span-priority 100) + (defun proof-highlight-depcs (name nmspans) (let ((helpmsg (concat "This item is a dependency (ancestor) of " name))) (while nmspans (let ((span (cadar nmspans))) (set-span-property span 'face 'proof-highlight-dependency-face) + (set-span-property span 'priority pg-dep-span-priority) (set-span-property span 'mouse-highlight nil) (set-span-property span 'help-echo helpmsg)) (setq nmspans (cdr nmspans))))) @@ -188,6 +192,7 @@ If LIST is empty, return a disabled menu item with NAME." (while nmspans (let ((span (cadar nmspans))) (set-span-property span 'face 'proof-highlight-dependent-face) + (set-span-property span 'priority pg-dep-span-priority) (set-span-property span 'mouse-highlight nil) (set-span-property span 'help-echo helpmsg) (set-span-property span 'balloon-help helpmsg)) @@ -203,6 +208,7 @@ If LIST is empty, return a disabled menu item with NAME." (while span (pg-set-span-helphighlights span 'nohighlight) (set-span-property span 'face 'proof-locked-face) + (set-span-property span 'priority pg-ordinary-span-priority) (setq span (next-span span 'type)))))) |