michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(emacs/lean-syntax): highlight 'import/section/end/namespace/open' arguments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-05 18:38:35 -07:00
parent d48dbccb00
commit 8610330cc4
1 changed files with 19 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,9 +49,7 @@
st)) st))
(defconst lean-font-lock-defaults (defconst lean-font-lock-defaults
`((;; Types `((;; Keywords
(,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face)
;; Keywords
(,(rx symbol-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun" (,(rx symbol-start (or "calc" "have" "obtains" "show" "by" "in" "let" "forall" "fun"
"exists" "if" "then" "else" "assume" "take" "obtain" "from") symbol-end) "exists" "if" "then" "else" "assume" "take" "obtain" "from") symbol-end)
. font-lock-keyword-face) . font-lock-keyword-face)
@ -68,6 +66,22 @@
(zero-or-more (or whitespace "(" "{" "[")) (zero-or-more (or whitespace "(" "{" "["))
(group (zero-or-more (not whitespace)))) (group (zero-or-more (not whitespace))))
(2 'font-lock-function-name-face)) (2 'font-lock-function-name-face))
;; namespace/section "name"
(,(rx symbol-start
(group (or "namespace" "section" "end"))
symbol-end
(zero-or-more whitespace)
(group (zero-or-more (not whitespace)))
(zero-or-more whitespace)
line-end)
(2 'font-lock-function-name-face))
;; import "names"
(,(rx symbol-start
(group (or "import" "open"))
symbol-end
(group (zero-or-more any))
line-end)
(2 'font-lock-constant-face))
("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face)) ("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
;; place holder ;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
@ -78,6 +92,8 @@
(or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat") (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat")
symbol-end) symbol-end)
. 'font-lock-constant-face) . 'font-lock-constant-face)
;; Types
(,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face)
;; sorry ;; sorry
(,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face) (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face)
;; lean-keywords ;; lean-keywords