62 lines
1.9 KiB
EmacsLisp
62 lines
1.9 KiB
EmacsLisp
;;; syd-lang-agda.el -*- lexical-binding: t; -*-
|
|
|
|
(with-eval-after-load 'agda2
|
|
(general-define-key
|
|
:keymaps 'agda2-mode-map
|
|
:states '(normal visual motion emacs insert)
|
|
:major-modes t
|
|
:prefix syd-localleader-key
|
|
:non-normal-prefix syd-alt-localleader-key
|
|
"?" #'agda2-show-goals
|
|
"." #'agda2-goal-and-context-and-inferred
|
|
"," #'agda2-goal-and-context
|
|
"=" #'agda2-show-constraints
|
|
"g" #'agda2-give
|
|
"a" #'agda2-mimer-maybe-all
|
|
"[" #'agda2-previous-goal
|
|
"c" #'agda2-make-case
|
|
"d" #'agda2-infer-type-maybe-toplevel
|
|
"e" #'agda2-show-context
|
|
"]" #'agda2-next-goal
|
|
"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
|
|
"x c" #'agda2-compile
|
|
"x d" #'agda2-remove-annotations
|
|
"x h" #'agda2-display-implicit-arguments
|
|
"x q" #'agda2-quit
|
|
"x r" #'agda2-restart)
|
|
(general-def
|
|
:keymaps 'agda2-mode-map
|
|
:states '(motion normal)
|
|
"[ n" #'agda2-previous-goal
|
|
"] n" #'agda2-next-goal)
|
|
(setq agda2-fontset-name "JuliaMono")
|
|
|
|
;; Inform Smartparens and Evil-surround of some extra brackets.
|
|
(with-eval-after-load 'smartparens
|
|
(sp-local-pair 'agda2-mode "⟨" "⟩"))
|
|
(syd-add-hook 'agda2-mode-hook
|
|
(defun syd-agda--configure-evil-surround-h ()
|
|
(with-eval-after-load 'evil-surround
|
|
(push '(?z . ("⟨" . "⟩"))
|
|
evil-surround-pairs-alist))))
|
|
|
|
(defun syd-agda-lookup-documentation ()
|
|
(interactive)
|
|
(call-interactively #'agda2-goal-and-context)
|
|
agda2-info-buffer)
|
|
|
|
;; DEPRECATED: Remove once syd-strategies is working.
|
|
(syd-add-hook 'agda2-mode-hook
|
|
(defun syd-agda-set-handlers-h ()
|
|
(setq-local syd-lookup-documentation-handlers
|
|
(list #'syd-agda-lookup-documentation)))))
|
|
|
|
(provide 'syd-lang-agda)
|