idris layer: rename the layer to idris-lang, update bindings and doc
Rename the layer to idris-lang because idris-packages variable is used by the package Update key bindings to better fit spacemacs conventions Convert markdown README to org
This commit is contained in:
syl20bnr
parent
c55c7c74a4
commit
2ccea679da
107
contrib/!lang/idris-lang/README.org
Normal file
107
contrib/!lang/idris-lang/README.org
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
# Idris contribution layer for Spacemacs
|
||||
|
||||
[[file:img/idris.png]]
|
||||
|
||||
* Table of Contents :TOC@4:
|
||||
- [[#description][Description]]
|
||||
- [[#install][Install]]
|
||||
- [[#layer][Layer]]
|
||||
- [[#idris][Idris]]
|
||||
- [[#key-bindings][Key bindings]]
|
||||
- [[#shorthands][Shorthands]]
|
||||
- [[#interactive-editing][Interactive editing]]
|
||||
- [[#documentation][Documentation]]
|
||||
- [[#repl][REPL]]
|
||||
- [[#active-term-manipulations][Active term manipulations]]
|
||||
- [[#build-system][Build system]]
|
||||
|
||||
* Description
|
||||
This layer adds support for the [[http://www.idris-lang.org/][Idris]] language.
|
||||
|
||||
* Install
|
||||
|
||||
** Layer
|
||||
To use this layer, add it to your =~/.spacemacs=
|
||||
|
||||
#+BEGIN_SRC emacs-lisp
|
||||
(setq-default dotspacemacs-configuration-layers '(idris))
|
||||
#+END_SRC
|
||||
|
||||
** Idris
|
||||
|
||||
Idris can be installed using =Haskell's cabal=:
|
||||
|
||||
#+BEGIN_SRC sh
|
||||
cabal install idris
|
||||
#+END_SRC
|
||||
|
||||
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~.
|
||||
|
Before Width: | Height: | Size: 4.9 KiB After Width: | Height: | Size: 4.9 KiB |
89
contrib/!lang/idris-lang/packages.el
Normal file
89
contrib/!lang/idris-lang/packages.el
Normal file
|
|
@ -0,0 +1,89 @@
|
|||
;;; packages.el --- Idris Layer packages File for Spacemacs
|
||||
;;
|
||||
;; Copyright (c) 2012-2014 Sylvain Benner
|
||||
;; Copyright (c) 2015 Timothy Jones
|
||||
;;
|
||||
;; Author: Timothy Jones <git@zmthy.io>
|
||||
;; URL: https://github.com/syl20bnr/spacemacs
|
||||
;;
|
||||
;; This file is not part of GNU Emacs.
|
||||
;;
|
||||
;;; License: GPLv3
|
||||
|
||||
;; We name this layer idris-lang instead of idris because
|
||||
;; the variable `idris-packages' is already used by `idris-mode'
|
||||
(setq idris-lang-packages '(idris-mode))
|
||||
|
||||
(defun idris-lang/init-idris-mode ()
|
||||
(use-package idris-mode
|
||||
:defer t
|
||||
:init
|
||||
(progn
|
||||
(defun spacemacs/idris-load-file-and-focus (&optional set-line)
|
||||
"Pass the current buffer's file to the REPL and switch to it in
|
||||
`insert state'."
|
||||
(interactive "p")
|
||||
(idris-load-file set-line)
|
||||
(idris-pop-to-repl)
|
||||
(evil-insert-state))
|
||||
|
||||
(defun spacemacs/idris-load-forward-line-and-focus ()
|
||||
"Pass the next line to REPL and switch to it in `insert state'."
|
||||
(interactive)
|
||||
(idris-load-forward-line)
|
||||
(idris-pop-to-repl)
|
||||
(evil-insert-state))
|
||||
|
||||
(defun spacemacs/idris-load-backward-line-and-focus ()
|
||||
"Pass the previous line to REPL and switch to it in `insert state'."
|
||||
(interactive)
|
||||
(idris-load-backward-line)
|
||||
(idris-pop-to-repl)
|
||||
(evil-insert-state))
|
||||
|
||||
(evil-leader/set-key-for-mode 'idris-mode
|
||||
;; Shorthands: rebind the standard evil-mode combinations to the local
|
||||
;; leader for the keys not used as a prefix below.
|
||||
"mc" 'idris-case-split
|
||||
"md" 'idris-add-clause
|
||||
"mp" 'idris-proof-search
|
||||
"mr" 'idris-load-file
|
||||
"mt" 'idris-type-at-point
|
||||
"mw" 'idris-make-with-block
|
||||
|
||||
;; ipkg.
|
||||
"mbc" 'idris-ipkg-build
|
||||
"mbC" 'idris-ipkg-clean
|
||||
"mbi" 'idris-ipkg-install
|
||||
"mbp" 'idris-open-package-file
|
||||
|
||||
;; Interactive editing.
|
||||
"mia" 'idris-proof-search
|
||||
"mic" 'idris-case-split
|
||||
"mie" 'idris-make-lemma
|
||||
"mim" 'idris-add-missing
|
||||
"mir" 'idris-refine
|
||||
"mis" 'idris-add-clause
|
||||
"miw" 'idris-make-with-block
|
||||
|
||||
;; Documentation.
|
||||
"mha" 'idris-apropos
|
||||
"mhd" 'idris-docs-at-point
|
||||
"mhs" 'idris-type-search
|
||||
"mht" 'idris-type-at-point
|
||||
|
||||
;; Active term manipulations.
|
||||
"mmn" 'idris-normalise-term
|
||||
"mmi" 'idris-show-term-implicits
|
||||
"mmh" 'idris-hide-term-implicits
|
||||
"mmc" 'idris-show-core-term
|
||||
|
||||
;; REPL
|
||||
"msb" 'idris-load-file
|
||||
"msB" 'spacemacs/idris-load-file-and-focus
|
||||
"msi" 'idris-ensure-process-and-repl-buffer
|
||||
"msn" 'idris-load-forward-line
|
||||
"msN" 'spacemacs/idris-load-forward-line-and-focus
|
||||
"msp" 'idris-load-backward-line
|
||||
"msP" 'spacemacs/idris-load-backward-line-and-focus
|
||||
"mss" 'idris-pop-to-repl))))
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
# Idris contribution layer for Spacemacs
|
||||
|
||||
|
||||
|
||||
<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc/generate-toc again -->
|
||||
**Table of Contents**
|
||||
|
||||
- [Idris contribution layer for Spacemacs](#idris-contribution-layer-for-spacemacs)
|
||||
- [Description](#description)
|
||||
- [Install](#install)
|
||||
- [Layer](#layer)
|
||||
- [Idris](#idris)
|
||||
- [Key bindings](#key-bindings)
|
||||
- [Shorthands](#shorthands)
|
||||
- [Interactive editing](#interactive-editing)
|
||||
- [Documentation](#documentation)
|
||||
- [File loading](#file-loading)
|
||||
- [Active term manipulations](#active-term-manipulations)
|
||||
- [Build system](#build-system)
|
||||
- [REPL](#repl)
|
||||
|
||||
<!-- markdown-toc end -->
|
||||
|
||||
## Description
|
||||
|
||||
This layer adds support for the [Idris][] language.
|
||||
|
||||
*This layer is in construction, it needs your contributions and bug reports.*
|
||||
|
||||
## Install
|
||||
|
||||
### Layer
|
||||
|
||||
To use this layer, add it to your `~/.spacemacs`
|
||||
|
||||
```elisp
|
||||
(setq-default dotspacemacs-configuration-layers '(idris))
|
||||
```
|
||||
|
||||
### Idris
|
||||
|
||||
Idris can be installed using Haskell's cabal:
|
||||
|
||||
```sh
|
||||
cabal install idris
|
||||
```
|
||||
|
||||
Binaries are also available for some platforms at
|
||||
http://www.idris-lang.org/download/
|
||||
|
||||
## Key bindings
|
||||
|
||||
All Idris specific bindings are prefixed with the major-mode leader <kbd>SPC
|
||||
m</kbd>.
|
||||
|
||||
### Shorthands
|
||||
|
||||
Several (but not all) of the evil-leader shorthands that `idris-mode` provides
|
||||
are reproduced under the local leader.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m r</kbd> | Load current buffer into Idris.
|
||||
<kbd>SPC m t</kbd> | Get the type for the identifier under point.
|
||||
<kbd>SPC m d</kbd> | Create an initial pattern match clause for a type declaration.
|
||||
<kbd>SPC m c</kbd> | Case split the pattern variable under point.
|
||||
<kbd>SPC m w</kbd> | Add a with block for the pattern-match clause under point.
|
||||
<kbd>SPC m p</kbd> | Attempt to solve a metavariable automatically.
|
||||
|
||||
### Interactive editing
|
||||
|
||||
Interactive editing commands are prefixed by <kbd>SPC m i</kbd>.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m i s</kbd> | Create an initial pattern match clause for a type declaration.
|
||||
<kbd>SPC m i m</kbd> | Add missing pattern-match cases to an existing definition.
|
||||
<kbd>SPC m i a</kbd> | Attempt to solve a metavariable automatically.
|
||||
<kbd>SPC m i e</kbd> | Extract a metavariable or provisional definition name to an explicit top level definition.
|
||||
<kbd>SPC m i c</kbd> | Case split the pattern variable under point.
|
||||
<kbd>SPC m i w</kbd> | Add a with block for the pattern-match clause under point.
|
||||
<kbd>SPC m i r</kbd> | Refine by name, without recursive proof search.
|
||||
|
||||
### Documentation
|
||||
|
||||
Documentation commands are prefixed by <kbd>SPC m h</kbd>.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m h d</kbd> | Search the documentation for the name under point.
|
||||
<kbd>SPC m h a</kbd> | Search the documentation for a string.
|
||||
<kbd>SPC m h s</kbd> | Search the documentation regarding a particular type.
|
||||
<kbd>SPC m h t</kbd> | Get the type for the identifier under point.
|
||||
|
||||
### File loading
|
||||
|
||||
File loading commands are prefixed by <kbd>SPC m l</kbd>.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m l b</kbd> | Load the current buffer into Idris.
|
||||
<kbd>SPC m l n</kbd> | Extend the region to be loaded, if such a region exists, one line at a time.
|
||||
<kbd>SPC m l p</kbd> | Contract the region to be loaded, if such a region exists, one line at a time.
|
||||
<kbd>SPC m l N</kbd> | Contract the region to be loaded, if such a region exists, one line at a time.
|
||||
|
||||
### Active term manipulations
|
||||
|
||||
Active term manipulations are prefixed by <kbd>SPC m m</kbd>.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m m n</kbd> | Normalize the term at point.
|
||||
<kbd>SPC m m i</kbd> | Show implicits for the term at point.
|
||||
<kbd>SPC m m h</kbd> | Hide implicits for the term at point.
|
||||
<kbd>SPC m m c</kbd> | Show the core language for the term at point.
|
||||
|
||||
### Build system
|
||||
|
||||
Commands for `ipkg` are prefixed by <kbd>SPC m b</kbd>.
|
||||
|
||||
Key Binding | Description
|
||||
---------------------|------------------------------------------------------------
|
||||
<kbd>SPC m b c</kbd> | Clean the package, removing `.ibc` files.`
|
||||
<kbd>SPC m b b</kbd> | Build the package.
|
||||
<kbd>SPC m b i</kbd> | Install the package to the user's repository, building first if necessary.
|
||||
|
||||
When inside a package file, you can insert a field with <kbd>SPC m f</kbd>.
|
||||
|
||||
### REPL
|
||||
|
||||
You can pop to the corresponding Idris REPL with <kbd>SPC m s</kbd>.
|
||||
|
||||
[Idris]: http://www.idris-lang.org/
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
;;; packages.el --- Idris Layer packages File for Spacemacs
|
||||
;;
|
||||
;; Copyright (c) 2012-2014 Sylvain Benner
|
||||
;; Copyright (c) 2015 Timothy Jones
|
||||
;;
|
||||
;; Author: Timothy Jones <git@zmthy.io>
|
||||
;; URL: https://github.com/syl20bnr/spacemacs
|
||||
;;
|
||||
;; This file is not part of GNU Emacs.
|
||||
;;
|
||||
;;; License: GPLv3
|
||||
|
||||
(setq idris-packages '(idris-mode))
|
||||
|
||||
(defun idris/init-idris-mode ()
|
||||
(use-package idris-mode
|
||||
:defer t
|
||||
:init
|
||||
(progn
|
||||
;; Ensure that the idris-define-evil-keys function has been defined, but
|
||||
;; not used, so that it can be overridden below.
|
||||
(require 'idris-keys)
|
||||
|
||||
;; Replace Idris' existing evil bindings with Spacemacs-style bindings.
|
||||
(defun idris-define-evil-keys ()
|
||||
"Define Spacemacs-style keys for evil-mode."
|
||||
(evil-leader/set-key-for-mode 'idris-mode
|
||||
;; Shorthands: rebind the standard evil-mode combinations to the local
|
||||
;; leader for the keys not used as a prefix below.
|
||||
"mc" 'idris-case-split
|
||||
"md" 'idris-add-clause
|
||||
"mp" 'idris-proof-search
|
||||
"mr" 'idris-load-file
|
||||
"mt" 'idris-type-at-point
|
||||
"mw" 'idris-make-with-block
|
||||
|
||||
;; Interactive editing.
|
||||
"mia" 'idris-proof-search
|
||||
"mic" 'idris-case-split
|
||||
"mie" 'idris-make-lemma
|
||||
"mim" 'idris-add-missing
|
||||
"mir" 'idris-refine
|
||||
"mis" 'idris-add-clause
|
||||
"miw" 'idris-make-with-block
|
||||
|
||||
;; Documentation.
|
||||
"mha" 'idris-apropos
|
||||
"mhd" 'idris-docs-at-point
|
||||
"mhs" 'idris-type-search
|
||||
"mht" 'idris-type-at-point
|
||||
|
||||
;; File loading.
|
||||
"mlb" 'idris-load-file
|
||||
"mln" 'idris-load-forward-line
|
||||
"mlp" 'idris-load-backward-line
|
||||
"mlN" 'idris-load-backward-line
|
||||
|
||||
;; Active term manipulations.
|
||||
"mmn" 'idris-normalise-term
|
||||
"mmi" 'idris-show-term-implicits
|
||||
"mmh" 'idris-hide-term-implicits
|
||||
"mmc" 'idris-show-core-term
|
||||
|
||||
;; ipkg.
|
||||
"mbb" 'idris-ipkg-build
|
||||
"mbc" 'idris-ipkg-clean
|
||||
"mbi" 'idris-ipkg-install
|
||||
"mbp" 'idris-open-package-file
|
||||
|
||||
;; Inferior mode switch.
|
||||
"ms" 'idris-pop-to-repl)
|
||||
|
||||
(evil-leader/set-key-for-mode 'idris-ipkg-mode
|
||||
"mf" 'idris-ipkg-insert-field)))
|
||||
|
||||
:config
|
||||
;; Idris also uses the idris-packages variable, so we clear it out in Idris
|
||||
;; buffers with a hook.
|
||||
(add-hook 'idris-mode-hook (lambda () (setq idris-packages nil)))))
|
||||
Loading…
Reference in a new issue