15
15
"Syntax highlighting for Agda."
18
(defcustom agda2-highlight-level 'non-interactive
19
"How much syntax highlighting should be produced?
20
Interactive highlighting includes highlighting of the expression
21
that is currently being type-checked."
23
(const :tag "None" none)
24
(const :tag "Non-interactive" non-interactive)
25
(const :tag "Interactive" interactive))
26
:group 'agda2-highlight)
28
(defun agda2-highlight-level nil
29
"Formats the highlighting level in a Haskelly way."
30
(cond ((equal agda2-highlight-level 'none) "None")
31
((equal agda2-highlight-level 'non-interactive) "NonInteractive")
32
((equal agda2-highlight-level 'interactive) "Interactive")
18
35
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
19
36
;; Functions for setting faces
161
184
font-lock-function-name-face))
162
185
(cons 'agda2-highlight-error-face
163
186
(agda2-highlight-face-attributes
164
font-lock-warning-face)))))))
187
font-lock-warning-face))
188
(cons 'agda2-highlight-typechecks-face
189
(agda2-highlight-face-attributes
190
font-lock-type-face))
191
(cons 'agda2-highlight-typechecking-face
192
(agda2-highlight-face-attributes
193
font-lock-preprocessor-face)))))))
166
195
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
169
198
(defcustom agda2-highlight-face-groups nil
170
199
"Colour scheme used in Agda buffers.
171
Note that changing this option does not remove the customisations
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."
200
Changes to this variable may not take full effect until you have
201
restarted Emacs. Note also that if you are using the
202
default-faces option and change your colour theme, then the
203
changes may not take effect in Agda buffers until you have
177
(const :tag "Use the settings below." nil)
178
(const :tag "Use an approximation of Conor McBride's colour scheme."
180
(const :tag "Use simplified highlighting and default font-lock faces."
206
(const :tag "Use the settings in the \"Agda2 Highlight Faces\" subgroup." nil)
207
(const :tag "Use an approximation of Conor McBride's colour scheme."
209
(const :tag "Use simplified highlighting and default font-lock faces."
182
211
:group 'agda2-highlight
183
212
:set 'agda2-highlight-set-faces)
214
(defgroup agda2-highlight-faces nil
215
"Faces used to highlight Agda code.
216
If `agda2-highlight-face-groups' is nil."
217
:group 'agda2-highlight)
185
219
(defface agda2-highlight-keyword-face
186
220
'((t (:foreground "DarkOrange3")))
187
221
"The face used for keywords."
188
:group 'agda2-highlight)
222
:group 'agda2-highlight-faces)
190
224
(defface agda2-highlight-string-face
191
225
'((t (:foreground "firebrick")))
192
226
"The face used for strings."
193
:group 'agda2-highlight)
227
:group 'agda2-highlight-faces)
195
229
(defface agda2-highlight-number-face
196
230
'((t (:foreground "purple")))
197
231
"The face used for numbers."
198
:group 'agda2-highlight)
232
:group 'agda2-highlight-faces)
200
234
(defface agda2-highlight-symbol-face
201
235
'((((background light))
203
237
(((background dark))
204
238
(:foreground "gray75")))
205
239
"The face used for symbols like forall, =, ->, etc."
206
:group 'agda2-highlight)
240
:group 'agda2-highlight-faces)
208
242
(defface agda2-highlight-primitive-type-face
209
243
'((t (:foreground "medium blue")))
210
244
"The face used for primitive types (like Set and Prop)."
211
:group 'agda2-highlight)
245
:group 'agda2-highlight-faces)
213
247
(defface agda2-highlight-bound-variable-face
215
249
"The face used for bound variables."
216
:group 'agda2-highlight)
250
:group 'agda2-highlight-faces)
218
252
(defface agda2-highlight-inductive-constructor-face
219
253
'((t (:foreground "green4")))
220
254
"The face used for inductive constructors."
221
:group 'agda2-highlight)
255
:group 'agda2-highlight-faces)
223
257
(defface agda2-highlight-coinductive-constructor-face
224
258
'((t (:foreground "gold4")))
225
259
"The face used for coinductive constructors."
226
:group 'agda2-highlight)
260
:group 'agda2-highlight-faces)
228
262
(defface agda2-highlight-datatype-face
229
263
'((t (:foreground "medium blue")))
230
264
"The face used for datatypes."
231
:group 'agda2-highlight)
265
:group 'agda2-highlight-faces)
233
267
(defface agda2-highlight-field-face
234
268
'((t (:foreground "DeepPink2")))
235
269
"The face used for record fields."
236
:group 'agda2-highlight)
270
:group 'agda2-highlight-faces)
238
272
(defface agda2-highlight-function-face
239
273
'((t (:foreground "medium blue")))
240
274
"The face used for functions."
241
:group 'agda2-highlight)
275
:group 'agda2-highlight-faces)
243
277
(defface agda2-highlight-module-face
244
278
'((t (:foreground "purple")))
245
279
"The face used for module names."
246
:group 'agda2-highlight)
280
:group 'agda2-highlight-faces)
248
282
(defface agda2-highlight-postulate-face
249
283
'((t (:foreground "medium blue")))
250
284
"The face used for postulates."
251
:group 'agda2-highlight)
285
:group 'agda2-highlight-faces)
253
287
(defface agda2-highlight-primitive-face
254
288
'((t (:foreground "medium blue")))
255
289
"The face used for primitive functions."
256
:group 'agda2-highlight)
290
:group 'agda2-highlight-faces)
258
292
(defface agda2-highlight-record-face
259
293
'((t (:foreground "medium blue")))
260
294
"The face used for record types."
261
:group 'agda2-highlight)
295
:group 'agda2-highlight-faces)
263
297
(defface agda2-highlight-dotted-face
265
299
"The face used for dotted patterns."
266
:group 'agda2-highlight)
300
:group 'agda2-highlight-faces)
268
302
(defface agda2-highlight-operator-face
270
304
"The face used for operators."
271
:group 'agda2-highlight)
305
:group 'agda2-highlight-faces)
273
307
(defface agda2-highlight-error-face
274
308
'((t (:foreground "red" :underline t)))
275
309
"The face used for errors."
276
:group 'agda2-highlight)
310
:group 'agda2-highlight-faces)
278
312
(defface agda2-highlight-unsolved-meta-face
279
313
'((t (:background "yellow"
280
314
:foreground "black")))
281
315
"The face used for unsolved meta variables."
282
:group 'agda2-highlight)
316
:group 'agda2-highlight-faces)
318
(defface agda2-highlight-unsolved-constraint-face
319
'((t (:background "yellow"
320
:foreground "black")))
321
"The face used for unsolved constraints which are not connected to metas."
322
:group 'agda2-highlight-faces)
284
324
(defface agda2-highlight-termination-problem-face
285
325
'((t (:background "light salmon"
286
326
:foreground "black")))
287
327
"The face used for termination problems."
288
:group 'agda2-highlight)
328
:group 'agda2-highlight-faces)
290
330
(defface agda2-highlight-incomplete-pattern-face
291
331
'((t (:background "wheat"
292
332
:foreground "black")))
293
333
"The face used for incomplete patterns. (Currently unused.)"
294
:group 'agda2-highlight)
334
:group 'agda2-highlight-faces)
336
(defface agda2-highlight-typechecks-face
337
'((t (:background "light blue"
338
:foreground "black")))
339
"The face used for code which is being type-checked."
340
:group 'agda2-highlight-faces)
296
342
(defvar agda2-highlight-faces
297
343
'((keyword . agda2-highlight-keyword-face)
349
400
table). The face `font-lock-comment-face' is used for comments.")
351
402
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
405
(defvar agda2-highlight-in-progress nil
406
"If nil, then highlighting annotations are not applied.")
407
(make-variable-buffer-local 'agda2-highlight-in-progress)
409
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
354
412
(defun agda2-highlight-setup nil
355
413
"Set up the `annotation' library for use with `agda2-mode'."
357
414
(setq annotation-bindings agda2-highlight-faces))
359
(defun agda2-highlight-load (file &optional keep)
416
(defun agda2-highlight-apply (&rest cmds)
417
"Adds the syntax highlighting information in the annotation list CMDS.
419
Old syntax highlighting information is not removed."
420
(let (;; Ignore read-only status, otherwise this function may fail.
421
(inhibit-read-only t))
422
(apply 'annotation-load
423
"Click mouse-2 to jump to definition"
426
(defun agda2-highlight-add-annotations (&rest cmds)
427
"Like `agda2-highlight-apply'.
428
But only if `agda2-highlight-in-progress' is non-nil."
429
(if agda2-highlight-in-progress
430
(apply 'agda2-highlight-apply cmds)))
432
(defun agda2-highlight-load (file)
360
433
"Load syntax highlighting information from FILE.
361
Old syntax highlighting information is first removed, unless KEEP
435
Old syntax highlighting information is not removed."
436
(let* ((coding-system-for-read 'utf-8)
437
(cmds (with-temp-buffer
438
(insert-file-contents file)
439
(goto-char (point-min))
440
(read (current-buffer)))))
441
(apply 'agda2-highlight-apply cmds)))
443
(defun agda2-highlight-load-and-delete-action (file)
444
"Like `agda2-highlight-load', but deletes FILE when done.
445
And highlighting is only updated if `agda2-highlight-in-progress'
363
(let ((coding-system-for-read 'utf-8)
364
;; Ignore read-only status, otherwise this function may fail.
365
(inhibit-read-only t))
366
(annotation-load-file file (lambda (anns) (not keep))
367
"Click mouse-2 to jump to definition")))
448
(if agda2-highlight-in-progress
449
(agda2-highlight-load file))
369
452
(defun agda2-highlight-clear nil
370
453
"Remove all syntax highlighting added by `agda2-highlight-reload'."
added
removed
src/data/emacs-mode/agda2-highlight.el
