74fdbb6795
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. |
||
|---|---|---|
| .. | ||
| config.el | ||
| packages.el | ||
| README.org | ||
Agda layer
Description
This layer adds support for the Agda programming language.
Some features:
- Faces redefined to correctly play with themes.
- Spacemacs bindings to Agda's interactive tools.
This layer is in construction, it needs your contributions and bug reports.
Install
Layer
To use this configuration layer, add it to your ~/.spacemacs. You will need to
add agda to the existing dotspacemacs-configuration-layers list in this
file.
Agda
Quick instructions to install Agda assuming you have cabal installed:
cabal install alex happy "cpphs < 1.19" agda
Then check that agda is available on your $PATH and seen by Emacs. For
information about setting up $PATH, check out the corresponding section in the
FAQ (SPC h SPC $PATH RET).
By default the agda-mode executable bundled with most agda installations is
used to locate the agda-mode package. If you don't have it and want to use a
local agda-mode package, you can customize the layer variable agda-mode-path
to your needs. Set it to nil if agda2.el is already discoverable in Emacs’
load path, otherwise set it to the path at which agda2.el can be found. For
example,
(agda2 :variables agda-mode-path "/some/path/to/agda2.el")Key bindings
The key bindings of this layer don't follow the Spacemacs conventions, we opted to a simple transcription of stock Agda mode key bindings to Spacemacs leader key.
All Agda specific bindings are prefixed with the major-mode leader
SPC m.
| Key Binding | Description |
|---|---|
SPC m = |
Show constraints. |
SPC m ? |
Show all goals. |
SPC m , |
Shows the type of the goal at point and the currect context. |
SPC m . |
Shows the context, the goal and the given expression's inferred type. |
SPC m a |
Simple proof search. |
SPC m b |
Go to the previous goal, if any and activate goal-navigation transient-state. |
SPC m c |
Refine the pattern variables given in the goal. |
SPC m d |
Infers the type of the given expression. |
SPC m e |
Show the context of the goal at point. |
SPC m f |
Go to the next goal, if any and activate goal-navigation transient-state. |
SPC m h |
Compute the type of a hypothetical helper function. |
SPC m l |
Load current buffer. |
SPC m n |
Computes the normal form of the given expression, using the scope of the current goal or, if point is not in a goal, the top-level scope. |
SPC m p |
Shows all the top-level names in the given module. |
SPC m r |
Refine the goal at point. |
SPC m s |
Solves all goals that are already instantiated internally. |
SPC m t |
Show the type of the goal at point. |
SPC m x c |
Compile current module. |
SPC m x d |
Removes buffer annotations (overlays and text properties). |
SPC m x h |
Toggle display of implicit arguments. |
SPC m x q |
Quit and clean up after agda2. |
SPC m x r |
Kill and restart the agda2 buffer and load agda2-toplevel-module. |
SPC m w |
Explains why a given name is in scope. |