From 70232f7ad959067eb6a077fc49cfe1264e24254c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Mar 2021 17:41:36 +0100 Subject: [PATCH] fix: lean4-mode: attributes are not documentation and in particular should not be spell-checked --- lean4-mode/lean4-syntax.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el index b4cebca996..e268a5d2f4 100644 --- a/lean4-mode/lean4-syntax.el +++ b/lean4-mode/lean4-syntax.el @@ -129,9 +129,9 @@ (defconst lean4-font-lock-defaults `((;; attributes (,(rx word-start "attribute" word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace)))) - (1 'font-lock-doc-face)) + (1 'font-lock-preprocessor-face)) (,(rx (group "@[" (zero-or-more (not (any "]"))) "]")) - (1 'font-lock-doc-face)) + (1 'font-lock-preprocessor-face)) (,(rx (group "#" (or "eval" "print" "reduce" "help" "check" "lang" "check_failure" "synth"))) (1 'font-lock-keyword-face)) ;; mutual definitions "names"