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

feat(emacs/lean-syntax): highlight mutual definitions, and attributes after definition keywords

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-12 20:37:34 -07:00
parent 8423f99043
commit 1983c94fb9
1 changed files with 25 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/emacs/lean-syntax.el
View file

@ -127,6 +127,21 @@
`((;; 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))
;; attributes after definitions
(,(rx word-start
(group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary"
"hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation"))
word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace)))
(zero-or-more whitespace)
(group (zero-or-more (not (any " \t\n\r{([")))))
(2 'font-lock-doc-face) (3 'font-lock-function-name-face))
;; attribute after mutual_definitions
(,(rx word-start
(group (or "mutual_definition" "mutual_meta_definition" "mutual_inductive"))
word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace)))
(zero-or-more whitespace)
(group (zero-or-more (not (any " \t\n\r{([,"))) (zero-or-more (zero-or-more whitespace) "," (zero-or-more whitespace) (not (any " \t\n\r{([,")))))
(2 'font-lock-doc-face) (3 'font-lock-function-name-face))
;; Constants which have a keyword as subterm
(,(rx (or "∘if")) . 'font-lock-constant-face)
;; Keywords
@ -142,14 +157,22 @@
;; ;; Constants
(,lean-constants-regexp . 'font-lock-constant-face)
(,lean-numerals-regexp . 'font-lock-constant-face)
;; universe/inductive/theorem... "names"
;; universe/inductive/theorem... "names" (without attributes)
(,(rx word-start
(group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary"
"hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation"))
word-end
(zero-or-more (or whitespace "(" "{" "["))
(zero-or-more whitespace)
(group (zero-or-more (not (any " \t\n\r{([")))))
(2 'font-lock-function-name-face))
;; meta_definitions "names" (without attributes)
(,(rx word-start
(group (or "mutual_definition" "mutual_meta_definition" "mutual_inductive"))
word-end
(zero-or-more whitespace)
(group (zero-or-more (not (any " \t\n\r{([,"))) (zero-or-more (zero-or-more whitespace) "," (zero-or-more whitespace) (not (any " \t\n\r{([,")))))
(2 'font-lock-function-name-face))
;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; warnings