Created
August 27, 2019 17:30
-
-
Save jesse-michael-han/e2b1f24dc7eb3ffc06f66412a9141c2e to your computer and use it in GitHub Desktop.
lean-mode customizations
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; jesse-michael-han's Emacs lean-mode hooks | |
;; append this to your init file (init.el or .emacs) | |
(require 'lean-mode) | |
(require 'lean-leanpkg) | |
(require 'smartparens) | |
(require 'company-lean) | |
(require 'yasnippet-lean) | |
(defun my-lean-insert-hole () | |
(interactive) | |
(insert "{!_!}") | |
(backward-char 3)) | |
(defun my-lean-insert-french () | |
(interactive) | |
(insert "‹_›")) | |
(defun lean-build-project () | |
(interactive) | |
(let ((dir (file-name-as-directory (lean-leanpkg-find-dir-safe))) | |
(lean-exe (f-full (lean-get-executable "leanpkg")))) | |
(let ((default-directory dir)) (compile (lean-compile-string lean-exe "build" ""))))) | |
(defun lean-test-project () | |
(interactive) | |
(let ((dir (file-name-as-directory (lean-leanpkg-find-dir-safe))) | |
(lean-exe (f-full (lean-get-executable "leanpkg")))) | |
(let ((default-directory dir)) (compile (lean-compile-string lean-exe "test" ""))))) | |
(defun lean-make-file () | |
(interactive) | |
(lean-execute "--make")) | |
(defun my-lean-mode-hook () | |
(company-quickhelp-mode) | |
(set-fringe-mode '(5 . 5)) ;; makes fringe larger so it's easier to see what lean is thinking about | |
(yas-minor-mode 1) | |
(local-set-key (kbd "C-c C-p C-f") 'lean-make-file) | |
(local-set-key (kbd "M-p") #'company-complete) | |
(local-set-key (kbd "C-c C-SPC") 'my-lean-insert-hole) ;; C-c C-SPC C-c SPC inserts a hole and opens menu of hole commands | |
(local-set-key (kbd "C-c C-f") 'my-lean-insert-french) | |
(local-set-key (kbd "C-c n") 'flycheck-next-error) | |
(local-set-key (kbd "C-c p") 'flycheck-previous-error) | |
(local-set-key (kbd "C-c C-s") 'sp-rewrap-sexp) ;; use for swapping implicit/explicitness of parameters | |
(local-set-key (kbd "C-c C-p C-b") 'lean-build-project) ;; opens compilation-mode buffer with hyperlinks to errors | |
(local-set-key (kbd "C-c C-p C-t") 'lean-test-project) | |
(define-key lean-mode-map (kbd "C-c C-t") 'lean-diff-types) | |
(lean-input-incorporate-changed-setting | |
'lean-input-user-translations | |
`( ("func" "⥤") | |
("McE" "ℰ") | |
("iP" "⨿") | |
("boxvert" "◫") | |
("no" "の") | |
("tf" "⟨╯°□°⟩╯︵┻━┻") )) | |
(column-number-mode) | |
(sp-local-pair 'lean-mode "⟨" "⟩") | |
(sp-local-pair 'lean-mode "⟦" "⟧") | |
(smartparens-mode)) | |
(add-hook 'lean-mode-hook 'my-lean-mode-hook) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Oops, I think that
require
is extraneous. It should be available afterlean-mode
is installed.