- Rename contrib directory to layers - Add new variable dotspacemacs-distribution - Move spacemacs layer to layers/!distribution - New layer spacemacs-core in layers/!distribution - User can now set dotspacemacs-distribution to spacemacs or spacemacs-core (default spacemacs) spacemacs-core is very lightweight layer sufficient to build upon spacemacs.
5.2 KiB
5.2 KiB
Idris contribution layer for Spacemacs
Table of Contents TOC@4
Description
This layer adds support for the Idris language.
Install
Layer
To use this layer, add it to your ~/.spacemacs
(setq-default dotspacemacs-configuration-layers '(idris))
Idris
Idris can be installed using Haskell's cabal
:
cabal install idris
Binaries are also available for some platforms at http://www.idris-lang.org/download/
Key bindings
Shorthands
Several (but not all) of the evil-leader shorthands that idris-mode
provides
are reproduced under the local leader.
Key Binding | Description |
---|---|
SPC m c |
Case split the pattern variable under point. |
SPC m d |
Create an initial pattern match clause for a type declaration. |
SPC m p |
Attempt to solve a metavariable automatically. |
SPC m r |
Load current buffer into Idris. |
SPC m t |
Get the type for the identifier under point. |
SPC m w |
Add a with block for the pattern-match clause under point. |
Interactive editing
Key Binding | Description |
---|---|
SPC m i a |
Attempt to solve a metavariable automatically. |
SPC m i c |
Case split the pattern variable under point. |
SPC m i e |
Extract a metavariable or provisional definition name to an explicit top level definition. |
SPC m i m |
Add missing pattern-match cases to an existing definition. |
SPC m i r |
Refine by name, without recursive proof search. |
SPC m i s |
Create an initial pattern match clause for a type declaration. |
SPC m i w |
Add a with block for the pattern-match clause under point. |
Documentation
Key Binding | Description |
---|---|
SPC m h a |
Search the documentation for a string. |
SPC m h d |
Search the documentation for the name under point. |
SPC m h s |
Search the documentation regarding a particular type. |
SPC m h t |
Get the type for the identifier under point. |
REPL
Key Binding | Description |
---|---|
SPC m s b |
Load the current buffer into Idris. |
SPC m s B |
Load the current buffer into Idris and switch to REPL in insert state |
SPC m s i |
Start Idris inferior process |
SPC m s n |
Extend the region to be loaded one line at a time. |
SPC m s N |
Extend the region to be loaded one line at a time and switch to REPL in insert state |
SPC m s p |
Contract the region to be loaded one line at a time |
SPC m s P |
Contract the region to be loaded one line at a time and switch to REPL in insert state |
SPC m s s |
Switch to REPL buffer |
Active term manipulations
Key Binding | Description |
---|---|
SPC m m c |
Show the core language for the term at point. |
SPC m m i |
Show implicits for the term at point. |
SPC m m h |
Hide implicits for the term at point. |
SPC m m n |
Normalize the term at point. |
Build system
Key Binding | Description |
---|---|
SPC m b c |
Build the package. |
SPC m b C |
Clean the package, removing .ibc files |
SPC m b i |
Install the package to the user's repository, building first if necessary. |
SPC m b p |
Open package file. |
When inside a package file, you can insert a field with SPC m f
.