From 2ccea679da94ac1292d8ef8be6fd633e07224e42 Mon Sep 17 00:00:00 2001 From: syl20bnr Date: Fri, 3 Jul 2015 20:10:27 -0400 Subject: [PATCH] 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 --- contrib/!lang/idris-lang/README.org | 107 ++++++++++++++ .../!lang/{idris => idris-lang}/img/idris.png | Bin contrib/!lang/idris-lang/packages.el | 89 ++++++++++++ contrib/!lang/idris/README.md | 133 ------------------ contrib/!lang/idris/packages.el | 79 ----------- 5 files changed, 196 insertions(+), 212 deletions(-) create mode 100644 contrib/!lang/idris-lang/README.org rename contrib/!lang/{idris => idris-lang}/img/idris.png (100%) create mode 100644 contrib/!lang/idris-lang/packages.el delete mode 100644 contrib/!lang/idris/README.md delete mode 100644 contrib/!lang/idris/packages.el diff --git a/contrib/!lang/idris-lang/README.org b/contrib/!lang/idris-lang/README.org new file mode 100644 index 000000000..732a65c3e --- /dev/null +++ b/contrib/!lang/idris-lang/README.org @@ -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~. diff --git a/contrib/!lang/idris/img/idris.png b/contrib/!lang/idris-lang/img/idris.png similarity index 100% rename from contrib/!lang/idris/img/idris.png rename to contrib/!lang/idris-lang/img/idris.png diff --git a/contrib/!lang/idris-lang/packages.el b/contrib/!lang/idris-lang/packages.el new file mode 100644 index 000000000..d02f4eb0c --- /dev/null +++ b/contrib/!lang/idris-lang/packages.el @@ -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 +;; 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)))) diff --git a/contrib/!lang/idris/README.md b/contrib/!lang/idris/README.md deleted file mode 100644 index cfad50286..000000000 --- a/contrib/!lang/idris/README.md +++ /dev/null @@ -1,133 +0,0 @@ -# Idris contribution layer for Spacemacs - -![logo](img/idris.png) - - -**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) - - - -## 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 SPC -m. - -### 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 r | Load current buffer into Idris. -SPC m t | Get the type for the identifier under point. -SPC m d | Create an initial pattern match clause for a type declaration. -SPC m c | Case split the pattern variable under point. -SPC m w | Add a with block for the pattern-match clause under point. -SPC m p | Attempt to solve a metavariable automatically. - -### Interactive editing - -Interactive editing commands are prefixed by SPC m i. - - Key Binding | Description ----------------------|------------------------------------------------------------ -SPC m i s | Create an initial pattern match clause for a type declaration. -SPC m i m | Add missing pattern-match cases to an existing definition. -SPC m i a | Attempt to solve a metavariable automatically. -SPC m i e | Extract a metavariable or provisional definition name to an explicit top level definition. -SPC m i c | Case split the pattern variable under point. -SPC m i w | Add a with block for the pattern-match clause under point. -SPC m i r | Refine by name, without recursive proof search. - -### Documentation - -Documentation commands are prefixed by SPC m h. - - Key Binding | Description ----------------------|------------------------------------------------------------ -SPC m h d | Search the documentation for the name under point. -SPC m h a | Search the documentation for a string. -SPC m h s | Search the documentation regarding a particular type. -SPC m h t | Get the type for the identifier under point. - -### File loading - -File loading commands are prefixed by SPC m l. - - Key Binding | Description ----------------------|------------------------------------------------------------ -SPC m l b | Load the current buffer into Idris. -SPC m l n | Extend the region to be loaded, if such a region exists, one line at a time. -SPC m l p | Contract the region to be loaded, if such a region exists, one line at a time. -SPC m l N | 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 SPC m m. - - Key Binding | Description ----------------------|------------------------------------------------------------ -SPC m m n | Normalize 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 c | Show the core language for the term at point. - -### Build system - -Commands for `ipkg` are prefixed by SPC m b. - - Key Binding | Description ----------------------|------------------------------------------------------------ -SPC m b c | Clean the package, removing `.ibc` files.` -SPC m b b | Build the package. -SPC m b i | Install the package to the user's repository, building first if necessary. - -When inside a package file, you can insert a field with SPC m f. - -### REPL - -You can pop to the corresponding Idris REPL with SPC m s. - -[Idris]: http://www.idris-lang.org/ diff --git a/contrib/!lang/idris/packages.el b/contrib/!lang/idris/packages.el deleted file mode 100644 index 3806cad85..000000000 --- a/contrib/!lang/idris/packages.el +++ /dev/null @@ -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 -;; 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)))))