TakeV/spacemacs
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
This repository has been archived on 2024-10-22. You can view files and clone it, but cannot push or open issues or pull requests.
spacemacs/layers/+lang/idris
History
syl20bnr 74fdbb6795 Refactor and simplify company backends declaration 
Enabling a company backend for a specific mode was a tedious tasks with code
scattered at different locations, one for local variable definitions, one for
company hook function definitions and another where the backends were pushed to
the local variables (which was problematic, since we ended up pushing the same
backends over and over again with `SPC f e R`, pushes have been replaced by
add-to-list calls in the new macro).

All these steps are now put together at one place with the new macro
spacemacs|add-company-backends, check its docstring for more info on its
arguments.

This macro also allows to define arbitrary buffer local variables to tune
company for specific modes (similar to layer variables via a keyword :variables)

The code related to company backends management has been moved to the
auto-completion layer in the funcs.el file. A nice side effect of this move is
that it enforces correct encapsulation of company backends related code. We can
now easily detect if there is some configuration leakage when the
auto-completion layer is not used. But we loose macro expansion at file loading
time (not sue it is a big concern though).

The function spacemacs|enable-auto-complete was never used so it has been
deleted which led to the deletion of the now empty file core-auto-completion.el.

The example in LAYERS.org regarding auto-completion is now out of date and has
been deleted. An example to setup auto-completion is provided in the README.org
file of the auto-completion layer.
2017-01-02 00:39:04 -05:00
..
img Rename the idris-lang layer to idris 2015-09-22 11:08:22 +02:00
packages.el Refactor and simplify company backends declaration 2017-01-02 00:39:04 -05:00
README.org Enable auto-complete in Idris repl 2016-07-02 12:41:49 +03:00

README.org

Idris layer

/TakeV/spacemacs/media/commit/74fdbb6795018a93a665fa2c417589cd4cbd51fc/layers/+lang/idris/img/idris.png

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, or make it into a case expression.
SPC m d Create an initial pattern match clause for a type declaration.
SPC m l Extract lemma from hole
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, or make it into a case expression.
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
SPC m s q Quit the Idris process

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.