Vim style bindings for idris2 mode

This commit is contained in:
Nathan McCarty 2023-06-24 05:15:30 -04:00
parent beafb54995
commit b6830c1621
Signed by: thatonelutenist
SSH Key Fingerprint: SHA256:hwQEcmak9E6sdU9bXc98RHw/Xd1AhpB5HZT7ZSVJkRM
1 changed files with 43 additions and 0 deletions

View File

@ -1048,18 +1048,61 @@ Disable company in idris2-mode, it's broken for now
(setq company-global-modes '(not idris2-mode idris2-repl-mode)))
#+end_src
Quick interactive function to restart the idris2 process when we have problems
#+begin_src emacs-lisp
(defun nm/idris2-restart ()
(interactive)
(idris2-quit)
(idris2-load-file))
#+end_src
Patch idris2-run via advice to pass through the environment, so that envrc will work properly.
We need to patch ~idris2-ru~, ~idris2-repl-buffer~, and the ~idris2-ipkg-command~ family
#+begin_src emacs-lisp
(after! idris2-mode
(require 'envrc)
(advice-add 'idris2-run :around #'envrc-propagate-environment)
(advice-add 'nm/idris2-restart :around #'envrc-propagate-environment)
(advice-add 'idris2-repl :around #'envrc-propagate-environment)
(advice-add 'idris2-repl-buffer :around #'envrc-propagate-environment)
(advice-add 'idris2-load-file :around #'envrc-propagate-environment)
(advice-add 'idris2-ipkg-command :around #'envrc-propagate-environment)
(advice-add 'idris2-ipkg-build :around #'envrc-propagate-environment)
(advice-add 'idris2-ipkg-clean :around #'envrc-propagate-environment))
#+end_src
Vim style bindings
#+begin_src emacs-lisp
(map! :after idris2-mode
:map idris2-mode-map
:localleader
"a" #'idris2-load-file
"b" #'idris2-proof-search
"d" #'idris2-case-dwim
"f" #'idris2-add-clause
"g" #'idris2-add-missing
"h" #'idris2-type-at-point
"j" #'idris2-jump-to-def-same-window
"k" #'idris2-docs-at-point
"l" #'idris2-pop-to-repl
";" #'idris2-type-search
"w" #'idris2-make-with-block
"e" #'idris2-make-lemma
"n" #'idris2-previous-error
"m" #'idris2-next-error
"z" #'idris2-apropos
(:prefix ("i" . "ipkg" )
"b" #'idris2-ipkg-build
"c" #'idris2-ipkg-clean
"o" #'idris2-open-package-file)
(:prefix ("r" . "repl")
"r" #'nm/idris2-restart
"c" #'idris2-compile-and-execute)
(:prefix ("p" . "prover")
"p" #'idris2-prove-hole))
#+end_src
** Haskell
Setup formatting
#+begin_src emacs-lisp