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

fix: lean4-mode: attributes are not documentation

Browse source 
and in particular should not be spell-checked
This commit is contained in:
Sebastian Ullrich 2021-03-09 17:41:36 +01:00
parent c2b357a5c8
commit 70232f7ad9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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"