/
idris-simple-indent.el
240 lines (212 loc) · 9.3 KB
/
idris-simple-indent.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
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
;;; idris-simple-indent.el --- Simple indentation module for Idris Mode
;; Copyright (C) 1998 Heribert Schuetz, Graeme E Moss
;; Author: Heribert Schuetz <Heribert.Schuetz@informatik.uni-muenchen.de>
;; Graeme E Moss <gem@cs.york.ac.uk>
;; Hacked for Idris by David Raymond Christiansen <david@davidchristiansen.dk>
;; Keywords: indentation files Idris
;; This file is not part of GNU Emacs.
;; This file 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, or (at your option)
;; any later version.
;; This file 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:
;; Purpose:
;;
;; To support simple indentation of Idris scripts.
;;
;;
;; Installation:
;;
;; To bind TAB to the indentation command for all Idris buffers, add
;; this to .emacs:
;;
;; (add-hook 'idris-mode-hook 'turn-on-idris-simple-indent)
;;
;; Otherwise, call `turn-on-idris-simple-indent'.
;;
;;
;; Customisation:
;;
;; None supported.
;;
;;
;; History:
;;
;; Version 0.1 - Initial version:
;; Imported from haskell-simple-indent 1.2
;;
;; Present Limitations/Future Work (contributions are most welcome!):
;;
;; (None so far.)
;;; Code:
;; All functions/variables start with
;; `(turn-(on/off)-)idris-simple-indent'.
(require 'idris-common-utils)
(defgroup idris-simple-indent nil
"Simple Idris indentation."
:link '(custom-manual "(idris-mode)Indentation")
:group 'idris
:prefix "idris-simple-indent-")
;; Version.
(defconst idris-simple-indent-version "0.1"
"`idris-simple-indent' version number.")
(defun idris-simple-indent-version ()
"Echo the current version of `idris-simple-indent' in the minibuffer."
(interactive)
(message "Using idris-simple-indent version %s"
idris-simple-indent-version))
(defun idris-simple-indent-current-indentation ()
"Return the indentation of the current line.
Takes into account literate Idris syntax."
(save-excursion
(move-to-column 0)
(looking-at (if (idris-lidr-p) ">\\s-*" "\\s-*"))
(length (match-string 0))))
(defun idris-simple-indent-indent-line-to (column)
"Indent current line to COLUMN.
Just like `indent-line-to', but ignoring the leading > for literate Idris."
(if (idris-lidr-p)
(if (save-excursion (move-to-column 0) (looking-at ">")) ;; lidr code line - look out for >
(progn
(save-excursion (move-to-column 0)
(re-search-forward ">\\s-*" nil t)
(replace-match (concat ">"
(if (<= column 1)
" "
(make-string (1- column) ? ))) nil nil))
(move-to-column column))
(indent-line-to column)) ;; in text part, do normal indent
(indent-line-to column))) ;; not lidr, do normal indent
(defun idris-simple-indent-tab-to-tab-stop ()
"A version of `tab-to-tab-stop' that takes literate Idris into account."
(let ((indent (idris-simple-indent-current-indentation))
(stops tab-stop-list)
indent-to)
(while (and stops (>= indent (car stops)))
(setq stops (cdr stops)))
(setq indent-to (if stops (car stops) 0))
(idris-simple-indent-indent-line-to indent-to)))
;; Partly stolen from `indent-relative' in indent.el:
(defun idris-simple-indent ()
"Space out to under next visible indent point.
Indent points are positions of non-whitespace following whitespace in
lines preceeding point. A position is visible if it is to the left of
the first non-whitespace of every nonblank line between the position and
the current line. If there is no visible indent point beyond the current
column, `tab-to-tab-stop' is done instead."
(interactive)
;; just insert two spaces for lidr if not on a code line
(if (and (idris-lidr-p)
(save-excursion (beginning-of-line) (not (looking-at-p ">"))))
(progn (beginning-of-line)
(insert " ")
(skip-chars-forward " "))
;; otherwise we're in code - do code indenting
(let* ((start-column (current-column))
(invisible-from nil) ; nil means infinity here
(indent
(catch 'idris-simple-indent-break
(save-excursion
(while (progn (beginning-of-line)
(not (bobp)))
(forward-line -1)
(if (not (if (idris-lidr-p) ;; if this line isn't whitespace-only
(or (looking-at ">[ \t]*\n") ;; whitespace only
(looking-at "[^>]")) ;; not code
(looking-at "[ \t]*\n")))
(let ((this-indentation (idris-simple-indent-current-indentation)))
(if (or (not invisible-from)
(< this-indentation invisible-from))
(if (> this-indentation start-column)
(setq invisible-from this-indentation)
(let ((end (line-beginning-position 2)))
(skip-chars-forward " \t" end)
;; Current indent + 2 is a valid stop
(if (= (current-column) start-column)
(forward-char 2)
(progn
(move-to-column start-column)
;; Is start-column inside a tab on this line?
(if (> (current-column) start-column)
(backward-char 1))
(or (looking-at "[ \t]")
(skip-chars-forward "^ \t" end))
(skip-chars-forward " \t" end)))
(let ((col (current-column)))
(throw 'idris-simple-indent-break
(if (or (= (point) end)
(and invisible-from
(> col invisible-from)))
invisible-from
col)))))))))))))
(if indent
(let ((opoint (point-marker)))
(idris-simple-indent-indent-line-to indent)
(if (> opoint (point))
(goto-char opoint))
(set-marker opoint nil))
(idris-simple-indent-tab-to-tab-stop)))))
(defun idris-simple-indent-backtab ()
"Indent backwards. Dual to `idris-simple-indent'."
(interactive)
(let ((current-indent (idris-simple-indent-current-indentation))
(indent-to (cons 0 0)))
(idris-simple-indent-indent-line-to 0)
(while (and (< (idris-simple-indent-current-indentation) (1- current-indent))
(<= (cdr indent-to) (car indent-to)))
(idris-simple-indent)
(setf (cdr indent-to) (car indent-to))
(setf (car indent-to) (idris-simple-indent-current-indentation)))
(idris-simple-indent-indent-line-to (cdr indent-to))))
(defun idris-simple-indent-newline-same-col ()
"Make a newline and go to the same column as the current line."
(interactive)
(let ((point (point)))
(let ((start-end
(save-excursion
(let* ((start (line-beginning-position))
(end (progn (goto-char start)
(search-forward-regexp
"[^ ]" (line-end-position) t 1))))
(when end (cons start (1- end)))))))
(if start-end
(progn (newline)
(insert (buffer-substring-no-properties
(car start-end) (cdr start-end))))
(newline)))))
;;;###autoload
(define-minor-mode idris-simple-indent-mode
"Simple Idris indentation mode that uses simple heuristic.
In this minor mode, `indent-for-tab-command' (bound to <tab> by
default) will move the cursor to the next indent point in the
previous nonblank line, whereas `idris-simple-indent-backtab'
\ (bound to <backtab> by default) will move the cursor the
previous indent point. An indent point is a non-whitespace
character following whitespace.
Runs `idris-simple-indent-hook' on activation."
:lighter " Ind"
:group 'idris-simple-indent
:keymap '(([backtab] . idris-simple-indent-backtab))
(kill-local-variable 'indent-line-function)
(when idris-simple-indent-mode
(set (make-local-variable 'indent-line-function) 'idris-simple-indent)
(run-hooks 'idris-simple-indent-hook)))
;; The main functions.
;;;###autoload
(defun turn-on-idris-simple-indent ()
"Turn on function `idris-simple-indent-mode'."
(interactive)
(idris-simple-indent-mode))
(defun turn-off-idris-simple-indent ()
"Turn off function `idris-simple-indent-mode'."
(interactive)
(idris-simple-indent-mode 0))
;; Provide ourselves:
(provide 'idris-simple-indent)
;;; idris-simple-indent.el ends here