- Syntax definition is developed based on the SublimeHaskell plugin using the AAAPackageDev plugin for converting
YAML
totmLanguage
. - [Interactive editing] Based on idris2-vim https://github.com/edwinb/idris2-vim/blob/master/doc/idris2-vim.txt#L41 functionality:
- It calls
idris2 --find-ipkg
with commands like:cs!
, just writing to your file. - The following commands are added to the Command Palette:
- ⌘ ` or ⌃ ⌘ T
Idris: Show type
(:t
for current symbol) - ⌃ ⌘ R
Idris: Reload
- ⌃ ⌘ C
Idris: Case split
(:cs!
for current symbol) - ⌃ ⌘ V
Idris: Add clause
(:ac!
for current symbol) - ⌃ ⌘ J
Idris: Add clause (pattern-matching proof)
(:apc!
for current symbol) - ⌃ ⌘ M
Idris: Add missing clauses
(:am!
for current symbol) - ⌃ ⌘ Y
Idris: Refine item
(:ref!
for current symbol) - ⌃ ⌘ S
Idris: Proof search
(:ps!
for current symbol) - ⌃ ⌘ O
Idris: Proof search with hints
(:ps!
for current symbol) - ⌃ ⌘ A
Idris: Generate definition
(:gd!
for current symbol) - ⌃ ⌘ L
Idris: Make lemma
(:ml!
for current symbol) - ⌃ ⌘ E
Idris: Evaluate expression
(any command for the REPL) - ⌃ ⌘ W
Idris: Make with pattern
(:ml!
for current symbol) - ⌃ ⌘ N
Idris: Make case
(:mc!
for current symbol) - ⌃ ⌘ H
Idris: Documentation
(:doc!
for current symbol)
- ⌘ ` or ⌃ ⌘ T
- It calls
-
Add this repository to Sublime Package Control. To do this, open up the command pallete with
Ctrl/Cmd + P
, start typing "repository" and choose the option "Package Control: Add Repository" when it comes up. Then paste the url (https://github.com/idris-hackers/idris-sublime) into the field at the bottom and press enter. -
Install the package. To do this, open the command pallete again, select "Package Control: Install Package", and choose
idris-sublime
. -
Re-open any
.idr
source files, and they will now be recognized as Idris source files.
Things that would be nice to have:
- Syntax definition for the literate source format
- Possibly some integration with SublimeREPL (idris support is almost there) + LoadFileTpRepl (idris is already there)