highlight names followed nameProviders in lean-mode

This commit is contained in:
Soonho Kong 2015-02-24 13:21:40 -05:00
commit 27ad846641

View file

@ -53,6 +53,9 @@ var leanHighlightRules = function() {
"universes", "using", "variable", "variables", "with"].join("|")
);
var nameProviders = (
["inductive", "structure", "record", "theorem", "axiom",
"axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
);
var storageType = (
@ -109,6 +112,8 @@ var leanHighlightRules = function() {
{defaultToken: "string"}
]
}, {
token : "keyword.control", regex : nameProviders, next : [
{token : "variable.language", regex : identifierRe, next : "start"} ]
}, {
token : "constant.numeric", // hex
regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"