148 lines
5.1 KiB
EmacsLisp
148 lines
5.1 KiB
EmacsLisp
;;; packages.el --- Idris Layer packages File for Spacemacs
|
|
;;
|
|
;; Copyright (c) 2012-2022 Sylvain Benner & Contributors
|
|
;;
|
|
;; Author: Timothy Jones <tim@zmthy.net>
|
|
;; URL: https://github.com/syl20bnr/spacemacs
|
|
;;
|
|
;; This file is not part of GNU Emacs.
|
|
;;
|
|
;; This program is free software; you can redistribute it and/or modify
|
|
;; it under the terms of the GNU General Public License as published by
|
|
;; the Free Software Foundation, either version 3 of the License, or
|
|
;; (at your option) any later version.
|
|
;;
|
|
;; This program is distributed in the hope that it will be useful,
|
|
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
;; GNU General Public License for more details.
|
|
;;
|
|
;; You should have received a copy of the GNU General Public License
|
|
;; along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
|
|
(setq idris-packages
|
|
'(
|
|
company
|
|
idris-mode
|
|
golden-ratio
|
|
popwin
|
|
))
|
|
|
|
(defun idris/post-init-company ()
|
|
(spacemacs|add-company-backends
|
|
:backends company-capf
|
|
:modes idris-mode idris-repl-mode))
|
|
|
|
(defun idris/init-idris-mode ()
|
|
(use-package idris-mode
|
|
:defer t
|
|
:init (spacemacs/register-repl 'idris-mode 'idris-repl "idris")
|
|
:config
|
|
(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))
|
|
|
|
;; 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-dwim
|
|
"d" 'idris-add-clause
|
|
"l" 'idris-make-lemma
|
|
"p" 'idris-proof-search
|
|
"r" 'idris-load-file
|
|
"t" 'idris-type-at-point
|
|
"w" 'idris-make-with-block
|
|
|
|
;; ipkg.
|
|
"bc" 'idris-ipkg-build
|
|
"bC" 'idris-ipkg-clean
|
|
"bi" 'idris-ipkg-install
|
|
"bp" 'idris-open-package-file
|
|
|
|
;; Interactive editing.
|
|
"ia" 'idris-proof-search
|
|
"ic" 'idris-case-dwim
|
|
"ie" 'idris-make-lemma
|
|
"im" 'idris-add-missing
|
|
"ir" 'idris-refine
|
|
"is" 'idris-add-clause
|
|
"iw" 'idris-make-with-block
|
|
|
|
;; Documentation.
|
|
"ha" 'idris-apropos
|
|
"hd" 'idris-docs-at-point
|
|
"hs" 'idris-type-search
|
|
"ht" 'idris-type-at-point
|
|
|
|
;; Active term manipulations.
|
|
"mn" 'idris-normalise-term
|
|
"mi" 'idris-show-term-implicits
|
|
"mh" 'idris-hide-term-implicits
|
|
"mc" 'idris-show-core-term
|
|
|
|
;; REPL
|
|
"'" 'idris-repl
|
|
"sb" 'idris-load-file
|
|
"sB" 'spacemacs/idris-load-file-and-focus
|
|
"si" 'idris-repl
|
|
"sn" 'idris-load-forward-line
|
|
"sN" 'spacemacs/idris-load-forward-line-and-focus
|
|
"sp" 'idris-load-backward-line
|
|
"sP" 'spacemacs/idris-load-backward-line-and-focus
|
|
"ss" 'idris-pop-to-repl
|
|
"sq" 'idris-quit)))
|
|
|
|
;; To suppress auto-indentation
|
|
(add-to-list 'spacemacs-indent-sensitive-modes 'idris-mode)
|
|
|
|
;; To bind TAB to the indentation command for all Idris buffers
|
|
(add-hook 'idris-mode-hook 'turn-on-idris-simple-indent)
|
|
|
|
;; open special buffers in motion state so they can be closed with ~q~
|
|
(evil-set-initial-state 'idris-compiler-notes-mode 'motion)
|
|
(evil-set-initial-state 'idris-hole-list-mode 'motion)
|
|
(evil-set-initial-state 'idris-info-mode 'motion))
|
|
|
|
(defun idris/pre-init-golden-ratio ()
|
|
(spacemacs|use-package-add-hook golden-ratio
|
|
:post-config
|
|
(dolist (x '("*idris-notes*" "*idris-holes*" "*idris-info*"))
|
|
(add-to-list 'golden-ratio-exclude-buffer-names x))))
|
|
|
|
(defun idris/pre-init-popwin ()
|
|
(spacemacs|use-package-add-hook popwin
|
|
:post-config
|
|
(push '("*idris-notes*" :dedicated t :position bottom :stick t :noselect nil :height 0.4)
|
|
popwin:special-display-config)
|
|
(push '("*idris-holes*" :dedicated t :position bottom :stick t :noselect nil :height 0.4)
|
|
popwin:special-display-config)
|
|
(push '("*idris-info*" :dedicated t :position bottom :stick t :noselect nil :height 0.4)
|
|
popwin:special-display-config)))
|