max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lean4-mode: enable semantic tokens by default

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-11 19:10:48 +01:00 • committed by Leonardo de Moura
parent cb5050bb7f
commit 92f75cf37b
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lean4-mode/lean4-mode.el
View file

@ -169,7 +169,9 @@ enabled and disabled respectively.")
;;(setq lean4-right-click-item-functions '(lean4-info-right-click-find-definition
;; lean4-hole-right-click))
;; Flycheck
(setq-local flycheck-disabled-checkers '()))
(setq-local flycheck-disabled-checkers '())
;; Lean massively benefits from semantic tokens, so change default to enabled
(setq-local lsp-semantic-tokens-enable t))
;; Automode List
;;;###autoload