idris-hackers/idris-sublime

A Plugin to use Idris with Sublime

Sublime Text plugin for Idris2 language

• Syntax definition is developed based on the SublimeHaskell plugin using the AAAPackageDev plugin for converting YAML to tmLanguage.
• [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)

Installation (with Sublime Package Control)

1. 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.

2. Install the package. To do this, open the command pallete again, select "Package Control: Install Package", and choose idris-sublime.

3. Re-open any .idr source files, and they will now be recognized as Idris source files.

TODO list

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)

idris-sublime's Issues

Highlighting is highly incorrect

Missing features:

• interface, implementation, namespace, export, and rewrite … in … are not colored as keywords
• Identifier names ending with multiple 's will cause all text after it being colored as string.
• Does not support 'identifier, "label-as-type".

cc. @edwinb

Please consider re-licensing this repository

Hello there, we'd love to use this library to syntax-highlight files on GitHub but in order to do so we need this library to have a more permissive license.

If you don't have any particular reason for choosing GPL would you be willing to consider switching this to a more permissive license such as MIT, BSD or Apache 2?

Many thanks
Arfon (GitHub Staff)

Add this plugin to the Package Control repository

People requested it here: laughedelic/sublime-idris#2.

• https://packagecontrol.io

Does not work with idris2 0.2.0 producing confusing error message

When plugin is used with 0.2.0 it tries to invoke idris2 with --find-ipkg. However 0.2.0 does not have this option and returns an error when invoked. idris-sublime subsequently reports that idris is not in PATH.

"implementation" and "interface" not seen as keywords

It seems that Github Linguist is using this repo as its source for highlighting Idris code. But it doesn't recognize the "interface" and "implementation" keywords.

Consider using Idris's IDE mode

Idris has a machine-readable REPL designed to make editor integration easy. Vim doesn't use it due to limitations in running subprocesses, but Atom and Emacs do. It provides things like richer semantic information for compiler output (tooltips with docstrings on names), extra commands, Agda-style semantic highlighting of source code, etc. I think this enables a nicer editor mode than --client.

Docs are here. If you're interested, I'm happy to answer questions, make tweaks that make your life easier, or improve the docs.