- Syntax definition is developed based on the SublimeHaskell plugin using the AAAPackageDev plugin for converting
YAML
totmLanguage
. WIP
Interactive editing functionality:- You have to start idris REPL server manually. Just execute
idris <your source files and modules>
(enumerating source files is necessary to avoid: openFile: does not exist (No such file or directory)
). - It calls
idris --client
with commands like:addclause!
, just writing to your file (it doesn't use--ideslave
). - There are some problems with this in idris itself: idris-vim#11 for example.
- The following commands are added to the Command Palette:
Idris: Run REPL command...
(any command for the REPL)Idris: Run editing command...
(this will be apended by the line number and the symbol name)Idris: Add clause
(:addclause!
for current symbol)Idris: Case split
(:casesplit!
for current symbol)Idris: Add missing clause
(:addmissing!
for current symbol)Idris: Proof search
(:proofsearch!
for current symbol)Idris: Make with pattern
(:makewith!
for current symbol)
- You have to start idris REPL server manually. Just execute
Things that would be nice to have:
- Optional keybindings
- Launch REPL server automatically
- Syntax definition for the literate source format
- Possibly some integration with SublimeREPL (idris support is almost there) + LoadFileTpRepl (idris is already there)
- Proper interaction with the
idris --ideslave
mode