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

fix(emacs/lean-syntax): syntax highlight, issue #306

Browse source 
1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
This commit is contained in:
Leonardo de Moura 2014-11-06 20:57:10 -08:00
parent 754901cf64
commit ed83b7ff2a
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -101,14 +101,15 @@
;; String ;; String
("\"[^\"]*\"" . 'font-lock-string-face) ("\"[^\"]*\"" . 'font-lock-string-face)
;; Constants ;; Constants
(,(rx (or "#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/")) . 'font-lock-constant-face) (,(rx symbol-start (or "#" "@" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/") symbol-end)
(,(rx (or "λ" "→" "∃" "∀" ":=")) . 'font-lock-constant-face ) . 'font-lock-constant-face)
(,(rx symbol-start (or "λ" "→" "∃" "∀" ":=") symbol-end) . 'font-lock-constant-face )
;; universe/inductive/theorem... "names" ;; universe/inductive/theorem... "names"
(,(rx word-start (,(rx word-start
(group (or "inductive" "structure" "record" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant")) (group (or "inductive" "structure" "record" "theorem" "axiom" "lemma" "hypothesis" "definition" "constant"))
word-end word-end
(zero-or-more (or whitespace "(" "{" "[")) (zero-or-more (or whitespace "(" "{" "["))
(group (zero-or-more (not (any " \t\n\r"))))) (group (zero-or-more (not (any " \t\n\r{([")))))
(2 'font-lock-function-name-face)) (2 'font-lock-function-name-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
@ -124,7 +125,8 @@
word-end) word-end)
. 'font-lock-constant-face) . 'font-lock-constant-face)
;; Types ;; Types
(,(rx symbol-start (or "Prop" "Type" "Type'" "Type₊" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face) (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₁" "Type₂" "Type₃") symbol-end) . 'font-lock-type-face)
(,(rx word-start (group "Type") ".") (1 'font-lock-type-face))
;; sorry ;; sorry
(,(rx word-start "sorry" word-end) . 'font-lock-warning-face) (,(rx word-start "sorry" word-end) . 'font-lock-warning-face)
;; extra-keywords ;; extra-keywords