40
40
:font 'unspecified)
41
41
(eval `(set-face-attribute face nil ,@attrs)))
43
(defvar agda2-highlight-face-attributes-list
44
'(:family :width :height :weight :slant :foreground :background
45
:inverse-video :stipple :underline :overline :strike-through
47
"The attributes considered by `agda2-highlight-face-attributes'.")
49
(defun agda2-highlight-face-attributes (face)
50
"The names and values of all attributes in FACE.
51
Only the attributes in `agda2-highlight-face-attributes-list' are
52
considered. The attributes are returned in a flat list of the
53
form (name1 value1 name2 value2...)."
55
(mapcar (lambda (attr)
56
(let ((val (face-attribute face attr)))
57
(if (member val '(unspecified nil)) '()
58
(list attr (if (symbolp val) `',val val)))))
59
agda2-highlight-face-attributes-list)))
43
61
(defun agda2-highlight-set-faces (variable group)
44
62
"Set all Agda faces according to the value of GROUP.
45
63
Also sets the default value of VARIABLE to GROUP."
88
106
:background "red")
89
107
(agda2-highlight-incomplete-pattern-face
90
108
:foreground "black"
91
:background "purple"))))))
109
:background "purple")))
110
((equal group 'default-faces)
111
(list (cons 'agda2-highlight-keyword-face
112
(agda2-highlight-face-attributes
113
font-lock-keyword-face))
114
(cons 'agda2-highlight-string-face
115
(agda2-highlight-face-attributes
116
font-lock-string-face))
117
(cons 'agda2-highlight-number-face
118
(agda2-highlight-face-attributes
119
font-lock-constant-face))
120
(cons 'agda2-highlight-symbol-face
121
(agda2-highlight-face-attributes
122
font-lock-keyword-face))
123
(cons 'agda2-highlight-primitive-type-face
124
(agda2-highlight-face-attributes
125
font-lock-keyword-face))
126
(cons 'agda2-highlight-bound-variable-face
127
(agda2-highlight-face-attributes
128
font-lock-variable-name-face))
129
(cons 'agda2-highlight-inductive-constructor-face
130
(agda2-highlight-face-attributes
131
font-lock-type-face))
132
(cons 'agda2-highlight-coinductive-constructor-face
133
(agda2-highlight-face-attributes
134
font-lock-type-face))
135
(cons 'agda2-highlight-datatype-face
136
(agda2-highlight-face-attributes
137
font-lock-type-face))
138
(cons 'agda2-highlight-field-face
139
(agda2-highlight-face-attributes
140
font-lock-variable-name-face))
141
(cons 'agda2-highlight-function-face
142
(agda2-highlight-face-attributes
143
font-lock-function-name-face))
144
(cons 'agda2-highlight-module-face
145
(agda2-highlight-face-attributes
146
font-lock-type-face))
147
(cons 'agda2-highlight-postulate-face
148
(agda2-highlight-face-attributes
149
font-lock-type-face))
150
(cons 'agda2-highlight-primitive-face
151
(agda2-highlight-face-attributes
152
font-lock-constant-face))
153
(cons 'agda2-highlight-record-face
154
(agda2-highlight-face-attributes
155
font-lock-variable-name-face))
156
(cons 'agda2-highlight-dotted-face
157
(agda2-highlight-face-attributes
158
font-lock-variable-name-face))
159
(cons 'agda2-highlight-operator-face
160
(agda2-highlight-face-attributes
161
font-lock-function-name-face))
162
(cons 'agda2-highlight-error-face
163
(agda2-highlight-face-attributes
164
font-lock-warning-face)))))))
93
166
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
96
169
(defcustom agda2-highlight-face-groups nil
97
"Colour scheme to use for agda2 highlight faces.
170
"Colour scheme used in Agda buffers.
98
171
Note that changing this option does not remove the customisations
99
172
below; you can get them back by resetting this option and
173
restarting Emacs. If you are using the default-faces option and
174
change your colour theme the changes may not take effect in Agda
175
buffers until you have restarted Emacs."
102
177
(const :tag "Use the settings below." nil)
103
178
(const :tag "Use an approximation of Conor McBride's colour scheme."
180
(const :tag "Use simplified highlighting and default font-lock faces."
105
182
:group 'agda2-highlight
106
183
:set 'agda2-highlight-set-faces)
274
351
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
277
(defun agda2-highlight-reload nil
278
"Reload current buffer's syntax information from the syntax file."
280
(let* ((dir (file-name-directory buffer-file-name))
281
(name (file-name-nondirectory buffer-file-name))
282
(file (concat dir "." name ".el"))
283
(inhibit-read-only t))
284
;; Ignore read-only status, otherwise this function may fail.
285
(annotation-load-file
287
;; Do not remove the old annotations if all the new ones
288
;; correspond to errors, or if there are no new ones.
289
(lambda (anns) (not (member anns '((error) nil))))
290
"Click mouse-2 to jump to definition")))
292
354
(defun agda2-highlight-setup nil
293
355
"Set up the `annotation' library for use with `agda2-mode'."
294
356
(font-lock-mode 0)
295
357
(setq annotation-bindings agda2-highlight-faces))
359
(defun agda2-highlight-load (file)
360
"Load syntax highlighting information from FILE."
361
(let ((coding-system-for-read 'utf-8)
362
;; Ignore read-only status, otherwise this function may fail.
363
(inhibit-read-only t))
364
(annotation-load-file file (lambda (anns) t)
365
"Click mouse-2 to jump to definition")))
297
367
(defun agda2-highlight-clear nil
298
368
"Remove all syntax highlighting added by `agda2-highlight-reload'."
301
371
; Ignore read-only status, otherwise this function may fail.
302
372
(annotation-remove-annotations)))
304
(defun agda2-highlight-reload-or-clear (&optional arg)
305
"Reload syntax highlighting information.
306
With prefix argument ARG: Remove syntax highlighting."
308
(if arg (agda2-highlight-clear)
309
(agda2-highlight-reload)))
311
374
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
312
375
;; Administrative details