idris-mode for emacs
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
font-lock-variable-name-face for operators) and done some
other things as appropriate for Idris.
used at all, for example, and data types declared with
data use the
same face as functions and values defined with
There are some docstrings spread around the mode, thus C-h m is helpful and returns the available key bindings. The REPL also supports tab completion, thus pressing tab opens a buffer with the available completions.
Some preliminary notes are available in the pdf
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.
inferior-idris-path if idris is not on your default path.
Place the elisp files somewhere in your load path and
Customize various aspects of the mode using
M-x customize-group RET idris RET.