Improve idris support
Squashing the 3 commits of #5688: Commit 1 -------- Add prefix doc in idris layer Also remove `idris-ensure-process-and-repl-buffer` as this is not an interactive command Add `SPC m l` keybinding for extracting lemma Bind `SPC m c` to `idris-case-dwim` Commit 2 -------- Fix registering idris repl Commit 3 -------- Add basic auto-completion for idris mode
This commit is contained in:
Jeremy Bi
Fabien Dubosson
parent
04ef674530
commit
ec9c18b832
|
|
@ -42,21 +42,22 @@ http://www.idris-lang.org/download/
|
|||
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. |
|
||||
| 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. |
|
||||
| ~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. |
|
||||
|
|
@ -77,7 +78,6 @@ are reproduced under the local leader.
|
|||
|-------------+----------------------------------------------------------------------------------------|
|
||||
| ~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 |
|
||||
|
|
|
|||
|
|
@ -0,0 +1,12 @@
|
|||
;;; config.el --- Idris Layer config File for Spacemacs
|
||||
;;
|
||||
;; Copyright (c) 2012-2016 Sylvain Benner & Contributors
|
||||
;;
|
||||
;; Author: Timothy Jones <git@zmthy.io>
|
||||
;; URL: https://github.com/syl20bnr/spacemacs
|
||||
;;
|
||||
;; This file is not part of GNU Emacs.
|
||||
;;
|
||||
;;; License: GPLv3
|
||||
|
||||
(spacemacs|defvar-company-backends idris-mode)
|
||||
|
|
@ -10,12 +10,16 @@
|
|||
;;; License: GPLv3
|
||||
|
||||
(setq idris-packages '(idris-mode
|
||||
company
|
||||
popwin))
|
||||
|
||||
(defun idris/post-init-company ()
|
||||
(spacemacs|add-company-hook idris-mode))
|
||||
|
||||
(defun idris/init-idris-mode ()
|
||||
(use-package idris-mode
|
||||
:defer t
|
||||
:init (spacemacs/register-repl 'idris-mode 'idris-ensure-process-and-repl-buffer "idris")
|
||||
:init (spacemacs/register-repl 'idris-mode 'idris-repl "idris")
|
||||
:config
|
||||
(progn
|
||||
(defun spacemacs/idris-load-file-and-focus (&optional set-line)
|
||||
|
|
@ -40,11 +44,19 @@
|
|||
(idris-pop-to-repl)
|
||||
(evil-insert-state))
|
||||
|
||||
;; prefix
|
||||
(spacemacs/declare-prefix-for-mode 'idris-mode "mb" "idris/build")
|
||||
(spacemacs/declare-prefix-for-mode 'idris-mode "mi" "idris/editing")
|
||||
(spacemacs/declare-prefix-for-mode 'idris-mode "mh" "idris/documentation")
|
||||
(spacemacs/declare-prefix-for-mode 'idris-mode "ms" "idris/repl")
|
||||
(spacemacs/declare-prefix-for-mode 'idris-mode "mm" "idris/term")
|
||||
|
||||
(spacemacs/set-leader-keys-for-major-mode 'idris-mode
|
||||
;; Shorthands: rebind the standard evil-mode combinations to the local
|
||||
;; leader for the keys not used as a prefix below.
|
||||
"c" 'idris-case-split
|
||||
"c" 'idris-case-dwim
|
||||
"d" 'idris-add-clause
|
||||
"l" 'idris-make-lemma
|
||||
"p" 'idris-proof-search
|
||||
"r" 'idris-load-file
|
||||
"t" 'idris-type-at-point
|
||||
|
|
@ -58,7 +70,7 @@
|
|||
|
||||
;; Interactive editing.
|
||||
"ia" 'idris-proof-search
|
||||
"ic" 'idris-case-split
|
||||
"ic" 'idris-case-dwim
|
||||
"ie" 'idris-make-lemma
|
||||
"im" 'idris-add-missing
|
||||
"ir" 'idris-refine
|
||||
|
|
@ -78,10 +90,8 @@
|
|||
"mc" 'idris-show-core-term
|
||||
|
||||
;; REPL
|
||||
"'" 'idris-ensure-process-and-repl-buffer
|
||||
"sb" 'idris-load-file
|
||||
"sB" 'spacemacs/idris-load-file-and-focus
|
||||
"si" 'idris-ensure-process-and-repl-buffer
|
||||
"sn" 'idris-load-forward-line
|
||||
"sN" 'spacemacs/idris-load-forward-line-and-focus
|
||||
"sp" 'idris-load-backward-line
|
||||
|
|
|
|||
Loading…
Reference in New Issue