From 92f75cf37b1c8ca52d37d678c49e842575acffb1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Mar 2021 19:10:48 +0100 Subject: [PATCH] feat: lean4-mode: enable semantic tokens by default --- lean4-mode/lean4-mode.el | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el index a41db98ed5..79826343ce 100644 --- a/lean4-mode/lean4-mode.el +++ b/lean4-mode/lean4-mode.el @@ -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