90 lines
2.8 KiB
EmacsLisp
90 lines
2.8 KiB
EmacsLisp
|
;;; 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))))
|