emacs.d/binds.el

;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; binds.el         ;;;;
;;;; Defines keybinds ;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;;
;;;; Global ;;;;
;;;;;;;;;;;;;;;;

;; Evil
(require 'evil)
(require 'evil-surround)
(require 'evil-commentary)
(require 'evil-leader)
(global-evil-leader-mode 1)
(evil-mode 1)
(evil-commentary-mode 1)
(global-undo-tree-mode 1)

;; Agda input mode ∀ buffers
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
(require 'agda-input)
(add-hook 'evil-insert-state-entry-hook (lambda ()
					  (if (not (eq major-mode 'latex-mode))
					      (set-input-method "Agda"))))
(add-hook 'evil-insert-state-exit-hook  (lambda () (set-input-method nil)))

;; No evil in certain modes
(add-hook 'vterm-mode-hook 'turn-off-evil-mode)
(add-hook 'zotero-browser-mode-hook 'turn-off-evil-mode)

;; Windowing
(define-prefix-command 'create-windows)
(global-set-key (kbd "C-a") 'create-windows)
(define-key create-windows (kbd "h") '(lambda () (interactive)
					    (split-window-right)
					    (evil-window-left 1)))
(define-key create-windows (kbd "j") '(lambda () (interactive)
					    (split-window-below)
					    (evil-window-down 1)))
(define-key create-windows (kbd "k") '(lambda () (interactive)
					    (split-window-below)
					    (evil-window-up 1)))
(define-key create-windows (kbd "l") '(lambda () (interactive)
					    (split-window-right)
					    (evil-window-right 1)))

(global-set-key (kbd "C-h") '(lambda () (interactive) (evil-window-left 1)))
(global-set-key (kbd "C-j") '(lambda () (interactive) (evil-window-down 1)))
(global-set-key (kbd "C-k") '(lambda () (interactive) (evil-window-up 1)))
(global-set-key (kbd "C-l") '(lambda () (interactive) (evil-window-right 1)))

(global-set-key (kbd "M-h") '(lambda () (interactive) (evil-window-decrease-width 1)))
(global-set-key (kbd "M-j") '(lambda () (interactive) (evil-window-decrease-height 1)))
(global-set-key (kbd "M-k") '(lambda () (interactive) (evil-window-increase-height 1)))
(global-set-key (kbd "M-l") '(lambda () (interactive) (evil-window-increase-width 1)))

(global-set-key (kbd "C-<return>") 'vterm)
(evil-global-set-key 'normal (kbd "C-t") 'treemacs)
(evil-global-set-key 'normal (kbd "C-d") 'evil-quit)
(evil-global-set-key 'emacs (kbd "C-t") 'treemacs)
(evil-global-set-key 'emacs (kbd "C-d") 'evil-quit)

;;;;;;;;;;;;;;;;;;;;;;;
;;;; Mode specific ;;;;
;;;;;;;;;;;;;;;;;;;;;;;

;; Elisp mode
(add-hook 'emacs-lisp-mode-hook
	  (lambda () (local-set-key (kbd "C-c C-l") 'eval-buffer)))

;; Agda mode
(evil-leader/set-leader "\\")
(add-hook
 'agda2-mode-hook
 (lambda ()
   (eval-after-load 'evil-maps
     '(evil-leader/set-key
        "a"  'agda2-auto-maybe-all
        "b"  'agda2-previous-goal
        "c"  'agda2-make-case
        "d"  'agda2-infer-type-maybe-toplevel
        "e"  'agda2-show-context
        "f"  'agda2-next-goal
        "h"  'agda2-helper-function-type
        "l"  'agda2-load
        "h"  'agda2-helper-function-type
        "n"  'agda2-compute-normalised-maybe-toplevel
        "o"  'agda2-module-contents-maybe-toplevel
        "r"  'agda2-refine
        "s"  'agda2-solve-maybe-all
        "t"  'agda2-goal-type
        "t"  'agda2-goal-type
        "w"  'agda2-why-in-scope-maybe-toplevel
        "z"  'agda2-search-about-toplevel
        "<SPC>"  'agda2-give
        "g"  'agda2-show-goals
        ","  'agda2-goal-and-context
        "."  'agda2-goal-and-context-and-inferred
        ";"  'agda2-goal-and-context-and-checked
        "="  'agda2-show-constraints
        "Gb" 'agda2-go-back
        "Gd" 'agda2-goto-definition-keyboard
        "xa" 'agda2-abort
        "xc" 'agda2-compile
        "xd" 'agda2-remove-annotations
        "xh" 'agda2-display-implicit-arguments
        "xt" 'agda2-display-irrelevant-arguments
        "xl" 'agda2-load
        "xq" 'agda2-quit
        "xr" 'agda2-restart
        "xs" 'agda2-set-program-version
        "x-" 'agda2-comment-dwim-rest-of-buffer))))