/usr/share/emacs/site-lisp/agda/annotation.el is in agda-mode 2.4.0.2-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 | ;;; annotation.el --- Functions for annotating text with faces and help bubbles
;;; Commentary:
;;
;;; Code:
(require 'cl)
(defconst annotations-offset (- (save-restriction (widen) (point-min)) 1)
"Offset between buffer positions and annotations's positions.
Annotations's positions are based on 1, so this adjusts it to the base
position used by your Emacs.")
(defvar annotation-bindings nil
"An association list mapping symbols to faces.")
(make-variable-buffer-local 'annotation-bindings)
(defvar annotation-goto-stack nil
"Positions from which `annotation-goto' was invoked.")
(defun annotation-goto-possible (pos)
"Return t if there's a hyperlink at the buffer position POS, and nil otherwise."
(if (get-text-property pos 'annotation-goto) t))
(defun annotation-goto-indirect (pos &optional other-window)
"Follow the `annotation-goto' hyperlink at position POS, if any.
If OTHER-WINDOW is t, use another window to display the given position."
(let ((previous-file-name buffer-file-name))
(if (and (annotation-goto (get-text-property pos 'annotation-goto)
other-window)
(not (eq (point) pos)))
(push `(,previous-file-name . ,pos) annotation-goto-stack))))
(defun annotation-go-back nil
"Go back to the previous position in which `annotation-goto' was
successfully invoked."
(when annotation-goto-stack
(let ((pos (pop annotation-goto-stack)))
(annotation-goto pos))))
(defun annotation-goto (filepos &optional other-window)
"Go to file position FILEPOS if the file is readable.
FILEPOS should have the form (FILE . POS). Return t if successful.
If OTHER-WINDOW is t, use another window to display the given
position."
(when (consp filepos)
(let ((file (car filepos)))
(if (file-readable-p file)
(progn
(if other-window
(find-file-other-window file)
(find-file file))
(goto-char (+ (cdr filepos) annotations-offset))
t)
(error "File does not exist or is unreadable: %s." file)))))
(defun annotation-annotate (start end anns &optional info goto)
"Annotate text between START and END in the current buffer.
Nothing happens if either START or END are out of bounds for the
current (possibly narrowed) buffer, or END <= START.
If ANNS is nil, then those text properties between START and END
that have been set by this function are deleted. Otherwise the
following happens.
All the symbols in ANNS are looked up in `annotation-bindings',
and the font-lock-face text property for the given character
range is set to the resulting list of faces.
If the string INFO is non-nil, the mouse-face
property is set to highlight, and INFO is used as the help-echo
string. If GOTO has the form (FILENAME . POSITION), then the
mouse-face property is set to highlight, and the given
filename/position will be used by `annotation-goto-indirect' when
it is invoked with a position in the given range.
Note that if a given attribute is defined by several faces, then
the first face's setting takes precedence.
All characters whose text properties get set also have the
annotation-annotated property set to t, and
annotation-annotations is set to a list with all the properties
that have been set; this ensures that the text properties can
later be removed (if the annotation-* properties are not tampered
with)."
(incf start annotations-offset)
(incf end annotations-offset)
(when (and (<= (point-min) start)
(< start end)
(<= end (point-max)))
(if (null anns)
(annotation-remove-annotations start end)
(let ((faces (delq nil
(mapcar (lambda (ann)
(cdr (assoc ann annotation-bindings)))
anns)))
(props nil))
(when faces
(put-text-property start end 'font-lock-face faces)
(add-to-list 'props 'font-lock-face))
(when (consp goto)
(add-text-properties start end
`(annotation-goto ,goto
mouse-face highlight))
(add-to-list 'props 'annotation-goto)
(add-to-list 'props 'mouse-face))
(when info
(add-text-properties start end
`(mouse-face highlight help-echo ,info))
(add-to-list 'props 'mouse-face)
(add-to-list 'props 'help-echo))
(when props
(let ((pos start)
mid)
(while (< pos end)
(setq mid (next-single-property-change pos
'annotation-annotations nil end))
(let* ((old-props (get-text-property pos 'annotation-annotations))
(all-props (union old-props props)))
(add-text-properties pos mid
`(annotation-annotated t annotation-annotations ,all-props))
(setq pos mid)))))))))
(defmacro annotation-preserve-mod-p-and-undo (&rest code)
"Run CODE preserving both the undo data and the modification bit.
Modification hooks are also disabled."
(let ((modp (make-symbol "modp")))
`(let ((,modp (buffer-modified-p))
;; Don't check if the file is being modified by some other process.
(buffer-file-name nil)
;; Don't record those changes on the undo-log.
(buffer-undo-list t)
;; Don't run modification hooks.
(inhibit-modification-hooks t))
(unwind-protect
(progn ,@code)
(restore-buffer-modified-p ,modp)))))
(defun annotation-remove-annotations (&optional start end)
"Remove all text properties set by `annotation-annotate'.
In the current buffer. If START and END are given, then
properties are only removed between these positions.
This function preserves the file modification stamp of the
current buffer, does not modify the undo list, and temporarily
disables all modification hooks.
Note: This function may fail if there is read-only text in the
buffer."
;; remove-text-properties fails for read-only text.
(annotation-preserve-mod-p-and-undo
(let ((pos (or start (point-min)))
pos2)
(while pos
(setq pos2 (next-single-property-change pos 'annotation-annotated
nil end))
(let ((props (get-text-property pos 'annotation-annotations)))
(when props
(remove-text-properties pos (or pos2 (point-max))
(mapcan (lambda (prop) (list prop nil))
(append '(annotation-annotated annotation-annotations)
props)))))
(setq pos (unless (equal pos2 end) pos2))))))
(defun annotation-load (goto-help &rest cmds)
"Apply highlighting annotations in CMDS in the current buffer.
The argument CMDS should be a list of lists (start end anns
&optional info goto). Text between start and end will be
annotated with the annotations in the list anns (using
`annotation-annotate'). If info and/or goto are present they will
be used as the corresponding arguments to `annotation-annotate'.
If INFO is nil in a call to `annotation-annotate', and the GOTO
argument is a cons-cell, then the INFO argument is set to
GOTO-HELP. The intention is that the default help text should
inform the user about the \"goto\" facility.
This function preserves the file modification stamp of the
current buffer, does not modify the undo list, and temporarily
disables all modification hooks.
Note: This function may fail if there is read-only text in the
buffer."
(annotation-preserve-mod-p-and-undo
(when (listp cmds)
(dolist (cmd cmds)
(destructuring-bind (start end anns &optional info goto) cmd
(let ((info (if (and (not info) (consp goto))
goto-help
info)))
(annotation-annotate start end anns info goto)))))))
(provide 'annotation)
;;; annotation.el ends here
|