emacs: lean4 support
This commit is contained in:
parent
c96a275fe3
commit
06b91b4456
21
spacemacs
21
spacemacs
|
|
@ -31,6 +31,7 @@ values."
|
|||
;; List of configuration layers to load.
|
||||
dotspacemacs-configuration-layers
|
||||
'(
|
||||
yaml
|
||||
html
|
||||
idris
|
||||
;; agda
|
||||
|
|
@ -145,11 +146,11 @@ values."
|
|||
dotspacemacs-colorize-cursor-according-to-state t
|
||||
;; Default font, or prioritized list of fonts. `powerline-scale' allows to
|
||||
;; quickly tweak the mode-line size to make separators look not too crappy.
|
||||
dotspacemacs-default-font '(;; "Source Code Pro"
|
||||
"Monospace Regular"
|
||||
:size 14
|
||||
;; :weight normal
|
||||
;; :width normal
|
||||
dotspacemacs-default-font '("Source Code Pro"
|
||||
;; "Monospace"
|
||||
:size 20
|
||||
:weight normal
|
||||
:width normal
|
||||
:powerline-scale 1.1)
|
||||
;; The leader key
|
||||
dotspacemacs-leader-key "SPC"
|
||||
|
|
@ -356,9 +357,9 @@ you should place your code here."
|
|||
|
||||
(setq evil-in-single-undo t)
|
||||
|
||||
(setq lean4-rootdir "~/lean4")
|
||||
; (setq lean4-rootdir "~/lean4")
|
||||
(add-to-load-path "~/lean4/lean4-mode")
|
||||
(setq lean4-rootdir "~/lean4")
|
||||
; (setq lean4-rootdir "~/lean4")
|
||||
(require 'lean4-mode)
|
||||
(push 'lean4-mode spacemacs-indent-sensitive-modes)
|
||||
|
||||
|
|
@ -370,7 +371,8 @@ you should place your code here."
|
|||
(remove 'evil-goto-definition spacemacs-default-jump-handlers))
|
||||
|
||||
(setq flycheck-display-errors-function nil) ; disable annoying flycheck tooltips
|
||||
(spacemacs|define-jump-handlers lean-mode lean-find-definition))
|
||||
;; (spacemacs|define-jump-handlers lean-mode lean-find-definition)
|
||||
)
|
||||
|
||||
|
||||
;; Do not write anything past this comment. This is where Emacs will
|
||||
|
|
@ -388,7 +390,6 @@ you should place your code here."
|
|||
;; If there is more than one, they won't work right.
|
||||
'(lean-server-show-pending-tasks t)
|
||||
'(package-selected-packages
|
||||
(quote
|
||||
(proof-general adaptive-wrap ws-butler winum which-key web-mode web-beautify volatile-highlights vi-tilde-fringe vdirel uuidgen use-package unfill toc-org tagedit spaceline solarized-theme smeargle slim-mode scss-mode sass-mode restart-emacs rainbow-delimiters racket-mode pug-mode popwin persp-mode pcre2el paradox ox-reveal orgit org-projectile org-present org-pomodoro org-mime org-download org-bullets open-junk-file noflet neotree mwim move-text mmm-mode markdown-toc magit-gitflow macrostep lorem-ipsum livid-mode linum-relative link-hint ledger-mode json-mode js2-refactor js-doc indent-guide idris-mode hungry-delete htmlize hl-todo highlight-parentheses highlight-numbers highlight-indentation helm-themes helm-swoop helm-projectile helm-mode-manager helm-make helm-lean helm-gitignore helm-flx helm-descbinds helm-css-scss helm-company helm-c-yasnippet helm-ag google-translate golden-ratio gnuplot gitconfig-mode gitattributes-mode git-timemachine git-messenger git-link git-gutter-fringe git-gutter-fringe+ gh-md fuzzy flycheck-pos-tip flycheck-ledger flx-ido fill-column-indicator fancy-battery eyebrowse expand-region exec-path-from-shell evil-visualstar evil-visual-mark-mode evil-unimpaired evil-tutor evil-surround evil-search-highlight-persist evil-numbers evil-nerd-commenter evil-mc evil-matchit evil-magit evil-lisp-state evil-indent-plus evil-iedit-state evil-exchange evil-escape evil-ediff evil-args evil-anzu eval-sexp-fu ensime emmet-mode elisp-slime-nav dumb-jump disaster diminish diff-hl define-word company-web company-tern company-statistics company-lean company-c-headers company-auctex column-enforce-mode coffee-mode cmake-mode clean-aindent-mode clang-format auto-yasnippet auto-highlight-symbol auto-compile auctex-latexmk aggressive-indent ace-window ace-link ace-jump-helm-line ac-ispell)))
|
||||
'(proof-general yaml-mode org-vcard org-category-capture log4e gntp skewer-mode json-snatcher json-reformat parent-mode request fringe-helper git-gutter+ git-gutter pos-tip flx anzu scala-mode diminish tern bind-map auto-complete pkg-info popup helm-lean persp-mode powerline alert multiple-cursors hydra projectile sbt-mode bind-key packed auctex company iedit smartparens highlight evil goto-chg yasnippet gitignore-mode flycheck epl f dash-functional avy magit magit-popup git-commit ghub let-alist with-editor markdown-mode js2-mode simple-httpd s helm helm-core async company-lean lean-mode org-mime racket-mode faceup winum unfill mu4e-maildirs-extension fuzzy web-mode tagedit slim-mode scss-mode sass-mode pug-mode less-css-mode helm-css-scss haml-mode emmet-mode company-web web-completion-data idris-mode prop-menu ws-butler window-numbering which-key web-beautify volatile-highlights vi-tilde-fringe vdirel uuidgen use-package toc-org spacemacs-theme spaceline solarized-theme smeargle restart-emacs rainbow-delimiters quelpa popwin pcre2el paradox ox-reveal orgit org-projectile org-present org-pomodoro org-plus-contrib org-download org-bullets open-junk-file noflet neotree mwim mu4e-alert move-text mmm-mode markdown-toc magit-gitflow macrostep lorem-ipsum livid-mode linum-relative link-hint ledger-mode json-mode js2-refactor js-doc info+ indent-guide ido-vertical-mode hungry-delete htmlize hl-todo highlight-parentheses highlight-numbers highlight-indentation hide-comnt help-fns+ helm-themes helm-swoop helm-projectile helm-mode-manager helm-make helm-gitignore helm-flx helm-descbinds helm-company helm-c-yasnippet helm-ag google-translate golden-ratio gnuplot gitconfig-mode gitattributes-mode git-timemachine git-messenger git-link git-gutter-fringe git-gutter-fringe+ gh-md flycheck-pos-tip flycheck-ledger flx-ido fill-column-indicator fancy-battery eyebrowse expand-region exec-path-from-shell evil-visualstar evil-visual-mark-mode evil-unimpaired evil-tutor evil-surround evil-search-highlight-persist evil-numbers evil-nerd-commenter evil-mc evil-matchit evil-magit evil-lisp-state evil-indent-plus evil-iedit-state evil-exchange evil-escape evil-ediff evil-args evil-anzu eval-sexp-fu ensime elisp-slime-nav dumb-jump disaster diff-hl define-word company-tern company-statistics company-c-headers company-auctex column-enforce-mode coffee-mode cmake-mode clean-aindent-mode clang-format auto-yasnippet auto-highlight-symbol auto-compile auctex-latexmk aggressive-indent adaptive-wrap ace-window ace-link ace-jump-helm-line ac-ispell))
|
||||
'(preview-auto-cache-preamble t)
|
||||
'(preview-scale-function 1.7))
|
||||
|
|
|
|||
Loading…
Reference in New Issue