aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-depends.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-03 21:38:56 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-03 21:38:56 +0000
commit86de6c069d01f236312c678d0f46e02abab46b01 (patch)
tree1f8b57b6944d97d3b32a74ad531ee75eecc73233 /generic/proof-depends.el
parent2cab60a0c0d886c9260ec69485ba4c1af4afa6e2 (diff)
Use pg-set-span-helphightlights for unhighlighting.
Diffstat (limited to 'generic/proof-depends.el')
-rw-r--r--generic/proof-depends.el11
1 files changed, 6 insertions, 5 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 9be21c7d..67a1f586 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -8,8 +8,7 @@
;;
;; $Id$
;;
-;; This file is based on Fiona McNeill's MSc project on
-;; analysing dependencies within proofs.
+;; Based on Fiona McNeill's MSc project on analysing dependencies within proofs.
;; Code rewritten by David Aspinall.
;;
@@ -185,18 +184,20 @@ If LIST is empty, return a disabled menu item with NAME."
(let ((span (cadar nmspans)))
(set-span-property span 'face 'proof-highlight-dependent-face)
(set-span-property span 'mouse-highlight nil)
- (set-span-property span 'help-echo helpmsg))
+ (set-span-property span 'help-echo helpmsg)
+ (set-span-property span 'balloon-help helpmsg))
(setq nmspans (cdr nmspans)))))
(defun proof-dep-unhighlight ()
"Returned all highlighted spans in file to the proof-locked-face highlighting."
(interactive)
- ;; FIXME: not quite right! Will highlight spans in queue as locked too.
+ ;; FIXME: not quite right! Will highlight spans in queue as locked too,
+ ;; and covers too many spans.
(save-excursion
(let ((span (span-at (point-min) 'type)))
(while span
+ (pg-set-span-helphighlights span 'nohighlight)
(set-span-property span 'face 'proof-locked-face)
- (set-span-property span 'help-echo nil)
(setq span (next-span span 'type))))))