From b6830c16213b0d8b5757820e8f4dffdabc7da9e3 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <nathan@mccarty.io>
Date: Sat, 24 Jun 2023 05:15:30 -0400
Subject: [PATCH] Vim style bindings for idris2 mode

---
 config.org | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/config.org b/config.org
index 7fee7e3..ee8ecdc 100644
--- a/config.org
+++ b/config.org
@@ -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