This is an emacs mode for editing Idris code.
Syntax highlighting functional languages is a little quirky; I've
deferred to haskell-mode for some things
(e.g. font-lock-variable-name-face
for operators) and done some
other things as appropriate for Idris. font-lock-type-face
isn't
used at all, for example, and data types declared with data
use the
same face as functions and values defined with =
.
There is now support for running an Idris interpreter in a buffer. Use 'C-c C-l' to load the current Idris buffer into the interpreter. This will spawn an inferior idris process and load the buffer. It will report warnings if idris reports any. Pressing C-c C-l again will reload that buffer - if you switch to a different buffer and press C-c C-l, that buffer will be loaded instead.
Customize inferior-idris-path
if idris is not on your default path.
Place the elisp files somewhere in your load path and (require 'idris-mode)
somewhere in ~/.emacs
or ~.emacs.d/init.el
.
Customize various aspects of the mode using M-x customize-group RET idris RET
.