79 lines
3.1 KiB
EmacsLisp
79 lines
3.1 KiB
EmacsLisp
;;; packages.el --- Agda2 Layer packages File for Spacemacs
|
|
;;
|
|
;; Copyright (c) 2012-2016 Sylvain Benner & Contributors
|
|
;;
|
|
;; Author: Oliver Charles <ollie@ocharles.org.uk>
|
|
;; URL: https://github.com/syl20bnr/spacemacs
|
|
;;
|
|
;; This file is not part of GNU Emacs.
|
|
;;
|
|
;;; License: GPLv3
|
|
|
|
(setq agda-packages
|
|
'((agda :location local)))
|
|
|
|
(defun agda/init-agda ()
|
|
(unless (executable-find "agda-mode")
|
|
(spacemacs-buffer/warning
|
|
(concat "Agda not detected, be sure that Agda binaries are "
|
|
"available in your PATH or check the installation "
|
|
"instructions in the README file.")))
|
|
|
|
(use-package agda2-mode
|
|
:if (executable-find "agda-mode")
|
|
:defer t
|
|
:init (load-file (let ((coding-system-for-read 'utf-8))
|
|
(shell-command-to-string "agda-mode locate")))
|
|
(mapc
|
|
(lambda (x) (add-to-list 'face-remapping-alist x))
|
|
'((agda2-highlight-datatype-face . font-lock-type-face)
|
|
(agda2-highlight-function-face . font-lock-type-face)
|
|
(agda2-highlight-inductive-constructor-face . font-lock-function-name-face)
|
|
(agda2-highlight-keyword-face . font-lock-keyword-face)
|
|
(agda2-highlight-module-face . font-lock-constant-face)
|
|
(agda2-highlight-number-face . nil)
|
|
(agda2-highlight-postulate-face . font-lock-type-face)
|
|
(agda2-highlight-primitive-type-face . font-lock-type-face)
|
|
(agda2-highlight-record-face . font-lock-type-face)))
|
|
:config
|
|
(progn
|
|
(spacemacs|define-transient-state goal-navigation
|
|
:title "Goal Navigation Transient State"
|
|
:doc "\n[_f_] next [_b_] previous [_q_] quit"
|
|
:bindings
|
|
("f" agda2-next-goal)
|
|
("b" agda2-previous-goal)
|
|
("q" nil :exit t))
|
|
(spacemacs/set-leader-keys-for-major-mode 'agda2-mode
|
|
"f" 'spacemacs/goal-navigation-transient-state/agda2-next-goal
|
|
"b" 'spacemacs/goal-navigation-transient-state/agda2-previous-goal)
|
|
|
|
(spacemacs/set-leader-keys-for-major-mode 'agda2-mode
|
|
"?" 'agda2-show-goals
|
|
"." 'agda2-goal-and-context-and-inferred
|
|
"," 'agda2-goal-and-context
|
|
"=" 'agda2-show-constraints
|
|
"SPC" 'agda2-give
|
|
"a" 'agda2-auto
|
|
"c" 'agda2-make-case
|
|
"d" 'agda2-infer-type-maybe-toplevel
|
|
"e" 'agda2-show-context
|
|
"gg" 'agda2-goto-definition-keyboard
|
|
"gG" 'agda2-go-back
|
|
"h" 'agda2-helper-function-type
|
|
"l" 'agda2-load
|
|
"n" 'agda2-compute-normalised-maybe-toplevel
|
|
"p" 'agda2-module-contents-maybe-toplevel
|
|
"r" 'agda2-refine
|
|
"s" 'agda2-solveAll
|
|
"t" 'agda2-goal-type
|
|
"w" 'agda2-why-in-scope-maybe-toplevel
|
|
"xc" 'agda2-compile
|
|
"xd" 'agda2-remove-annotations
|
|
"xh" 'agda2-display-implicit-arguments
|
|
"xq" 'agda2-quit
|
|
"xr" 'agda2-restart)
|
|
|
|
(with-eval-after-load 'golden-ratio
|
|
(add-to-list 'golden-ratio-exclude-buffer-names
|
|
"*Agda information*")))))
|