82fdd9a511
Motivation While disabling Evil in holy-mode makes its implementation shorter and sounds elegant on the paper, in practice it puts a big burden on the configuration parts which need to know if Evil is enable or not. This is a bad separation of concerns and the bunch of fixes that we were forced to do in the past weeks shows this issue. Those fixes were about removing the knowledge of the activation of Evil by implementing new dispatching functions to be used by layers, this is cumbersome and makes Spacemacs layer configuration more subtle which is not good. There was additional bad consequences of the removal of Evil state like the impossibility to use Evil lisp state or iedit states, or we would have been forced to implement a temporary activation of Evil which is awkward. Instead I reintroduce Evil as the central piece of Spacemacs design thus Evil is now re-enabled in holy-mode. It provides the abstraction we need to isolate editing styles and be able to grow the Spacemacs configuration coverage sanely. Layers don't need to check whether the holy mode is active or not and they don't need to know if Evil is available (it is always available). We also don't need to write additional dispatching functions, this is the job of Evil, and I think it provides everything for this. Ideally configuration layer should be implemented with only Evil in mind and the holy-mode (and hybrid-mode) should magically make it work for Emacs style users, for instance we can freely use `evil-insert-state` anywhere in the code without any guard. Evil is now even more part of Spacemacs, we can really say that Spacemacs is Emacs+Evil which is now an indivisible pair. Spacemacs needed this stable API to continue on the right track. While these changes should be rather transparent to the user, I'm sorry for this experimental period, I failed to see all the implications of such a change, I was just excited about the possibility to make Evil optional. The reality is that Spacemacs has to embrace it and keep its strong position on being Emacs+Evil at the core. Implementation - insert, motion and normal states are forced to emacs state using an advice on `evil-insert-state`, `evil-motion-state` and `evil-normal-state` respectively. These functions can be used freely in the layer configuration. - A new general hook `spacemacs-editing-style-hook` allow to hook any code that need to be configured based on the editing style. Functions hooked to this hook takes the current style as parameter, this basically generalize the hook used to setup hjkl navigation bindings. - ESC has been removed from the emacs state map. - Revert unneeded changes - Revert "evil: enter insert-state only from normal-state" commit |
||
---|---|---|
.. | ||
img | ||
packages.el | ||
README.org |
Idris layer
Description
This layer adds support for the Idris language.
Install
Layer
To use this configuration layer, add it to your ~/.spacemacs
. You will need to
add idris
to the existing dotspacemacs-configuration-layers
list in this
file.
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
.