Idris for Visual Studio Code

Implemented features

Heads up: All the commands above can also be triggered in the right-click menu

• iPKG
• Auto-completion
• Show type definition on hover
• Type checking on saving file
• Go to Definition and Peek Definition
• Go to Symbol (Outline symbols in currently opend file)
• Search Symbol (Outline symbols in currently opend project)
• Find all references
• Rename symbol
• Change all occurrences
• Latex snippets
• Literate Idris
• Document highlights
• Parameter hints

Installation

1. Within Visual Studio Code, open the command palette (Ctrl-Shift-P / Cmd-Shift-P).
2. Select Install Extension and search for Idris or run ext install Idris.
3. Download Idris and make sure the idris executable is on your PATH.
4. Run cabal install idringen and make sure the idrin executable is on your PATH.

Contributing

Check out CONTRIBUTING.md.

Options

The following Visual Studio Code settings along with their default values that are available for the Idris extension. If you want to change any of these, you can do so in user preferences (cmd+,) or workspace settings (.vscode/settings.json). You don't have to copy these if you don't intend to change them.

{
    "idris.executablePath": "idris",            // The full path to the idris executable.
    "idris.hoverMode": "fallback",              // Controls the hover behavior. 'info' will display Idris documentation, 'type' will display Idris type, 'fallback' will try 'info' first and fallback to 'type' if we can not get the documentation, and 'none' will disable hover tooltips.
    "idris.suggestMode": "allWords"             // Controls the auto-completion behavior. 'allWords' will always include all words from the currently opened documentation, 'replCompletion' will get suggestions from Idris REPL process.
    "idris.warnPartial": false                  // Show warning when a function is partial.
    "idris.showOutputWhenTypechecking": false   //Show output channel when typechecking finished.
    "idris.numbersOfContinuousTypechecking": 10 //Kill Idris process every N times of continuous typechecking to avoid memory leaking.
}

Acknowledgements

• The internal design is initially inspired by atom-language-idris.

Thanks

• Belleve Invis @be5invis (The maintainer of the syntax files)

License

BSD 3-Clause, the same as Idris.