/
idris-highlight-input.el
147 lines (127 loc) · 6.59 KB
/
idris-highlight-input.el
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
;;; idris-highlight-input.el --- Compiler-driven highlighting of user input -*- lexical-binding: t; -*-
;; Copyright (C) 2015 David Raymond Christiansen
;; Author: David Raymond Christiansen <david@davidchristiansen.dk>
;; Keywords: languages
;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.
;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;; GNU General Public License for more details.
;; You should have received a copy of the GNU General Public License
;; along with this program. If not, see <http://www.gnu.org/licenses/>.
;;; Commentary:
;; This file contains routines for highlighting user input with
;; information generated by the Idris elaborator.
;;; Code:
(require 'idris-common-utils)
(require 'idris-settings)
(defun idris-highlight-remove-overlays (&optional buffer)
"Remove all Idris highlighting overlays from BUFFER.
Use the current buffer if BUFFER is nil."
(interactive)
(with-current-buffer (or buffer (current-buffer))
(save-restriction
(widen)
(dolist (overlay (overlays-in (point-min) (point-max)))
(when (overlay-get overlay 'idris-source-highlight)
(delete-overlay overlay))))))
(defun idris-highlight-column (idris-col)
"Compute the Emacs position offset of the Idris column IDRIS-COL.
In particular, this takes bird tracks into account in literate Idris."
(+ idris-col (if (idris-lidr-p) 1 -1)))
(defun idris-highlight--overlay-modification-hook (&rest args)
"Delete semantic overlays if they are changed.
See Info node `(elisp)Overlay Properties' to understand how ARGS are used."
;; There are 5 args when it's called post-modification
(when (= (length args) 5)
(delete-overlay (car args))))
(defun idris-highlight-input-region (start-line start-col end-line end-col highlight)
"Highlight in BUFFER using an overlay from START-LINE and START-COL to
END-LINE and END-COL and the semantic properties specified in HIGHLIGHT."
(save-excursion
(save-restriction
(widen)
(goto-char (point-min))
(let* ((start-pos (+ (line-beginning-position start-line)
(idris-highlight-column start-col)))
(end-pos (+ (line-beginning-position end-line)
(idris-highlight-column end-col)))
(existing-idris-overlays-in-range (seq-filter
(lambda (overlay)
(overlay-get overlay 'idris-source-highlight))
(overlays-in start-pos end-pos)))
(existing-idris-overlay (seq-find (lambda (overlay)
(and
(eql start-pos (overlay-start overlay))
(eql end-pos (overlay-end overlay))
;; TODO: overlay properties match
))
existing-idris-overlays-in-range)))
(when (null existing-idris-overlay)
(mapc #'delete-overlay existing-idris-overlays-in-range)
(let ((highlight-overlay (make-overlay start-pos end-pos)))
(overlay-put highlight-overlay 'idris-source-highlight t)
(idris-add-overlay-properties highlight-overlay (idris-semantic-properties highlight))
(overlay-put highlight-overlay 'modification-hooks '(idris-highlight--overlay-modification-hook))))))))
(defun idris-highlight-source-file (hs)
(pcase-dolist
(`(((:filename ,fn)
(:start ,start-line-raw ,start-col-raw)
(:end ,end-line-raw ,end-col-raw))
,props)
hs)
(when (string= (file-name-nondirectory fn)
(file-name-nondirectory (buffer-file-name)))
(let ((start-line (if (>=-protocol-version 2 1)
(1+ start-line-raw)
start-line-raw))
(start-col (if (>=-protocol-version 2 1)
(1+ start-col-raw)
start-col-raw))
(end-line (if (>=-protocol-version 2 1)
(1+ end-line-raw)
end-line-raw))
(end-col (if (>= idris-protocol-version 1)
(1+ end-col-raw)
end-col-raw)))
(idris-highlight-input-region start-line start-col
end-line end-col
props)))))
(defun idris-highlight-input-region-debug (start-line start-col end-line end-col highlight)
(when (not (or (> end-line start-line)
(and (= end-line start-line)
(> end-col start-col))))
(message "Not highlighting absurd span %s:%s-%s:%s with %s"
start-line start-col
end-line end-col
highlight)))
(defun idris-toggle-semantic-source-highlighting ()
"Turn on/off semantic highlighting.
This is controled by value of `idris-semantic-source-highlighting' variable.
When the value is `debug' additional checks are performed on received data."
(if idris-semantic-source-highlighting
(progn
(if (eq idris-semantic-source-highlighting 'debug)
(advice-add 'idris-highlight-input-region
:before-until
#'idris-highlight-input-region-debug)
(advice-remove 'idris-highlight-input-region
#'idris-highlight-input-region-debug))
(advice-remove 'idris-highlight-source-file #'ignore))
(advice-add 'idris-highlight-source-file :around #'ignore)))
(defun idris-buffer-semantic-source-highlighting ()
"Return nil if current buffer size is larger than set limit.
The limit is defined as value of:
`idris-semantic-source-highlighting-max-buffer-size'.
Otherwise return current value of `idris-semantic-source-highlighting'"
(if (< (buffer-size)
idris-semantic-source-highlighting-max-buffer-size)
idris-semantic-source-highlighting
(message "Semantic source highlighting is disabled for the current buffer. %s"
"Customize `idris-semantic-source-highlighting-max-buffer-size' to enable it.")
nil))
(provide 'idris-highlight-input)
;;; idris-highlight-input.el ends here