799 |
(add-text-properties |
(add-text-properties |
800 |
(marker-position text-beg) (- (marker-position text-end) 1) |
(marker-position text-beg) (- (marker-position text-end) 1) |
801 |
'(mouse-face highlight |
'(mouse-face highlight |
802 |
help-echo "mouse-2: go to this occurence")) |
help-echo "mouse-2: go to this occurrence")) |
803 |
(put-text-property (marker-position text-beg) |
(put-text-property (marker-position text-beg) |
804 |
(marker-position text-end) |
(marker-position text-end) |
805 |
'occur occur-marker) |
'occur occur-marker) |