jyapayne/ace
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

add and sort keywords/storage-modifiers for lean-mode

Browse source
This commit is contained in:
Soonho Kong 2015-02-24 13:20:28 -05:00
commit 3c34a9852f
1 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

37
lib/ace/mode/lean_highlight_rules.js
View file

@ -38,20 +38,21 @@ var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
var leanHighlightRules = function() { var leanHighlightRules = function() {
var keywordControls = ( var keywordControls = (
["import", "tactic_hint", "protected", "find_decl", [ "add_rewrite", "alias", "as", "assume", "attribute",
"private", "opaque", "definition", "renaming", "hiding", "exposing", "begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
"parameter", "parameters", "begin", "proof", "qed", "conjecture", "premise", "premises", "classes", "coercions", "conjecture", "constants", "context",
"constant", "constants", "example", "attribute", "local", "corollary", "else", "end", "environment", "eval", "example",
"hypothesis", "lemma", "corollary", "variable", "variables", "print", "exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
"theorem", "context", "open", "as", "export", "axiom", "inductive", "forall", "from", "fun", "have", "help", "hiding", "if",
"with", "structure", "record", "universe", "universes", "alias", "help", "environment", "import", "in", "infix", "infixl", "infixr", "instances",
"options", "precedence", "postfix", "prefix", "calc_trans", "let", "local", "match", "namespace", "notation", "obtain", "obtains",
"calc_subst", "calc_refl", "infix", "infixl", "infixr", "notation", "omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
"eval", "check", "exit", "end", "using", "namespace", "precedence", "prefix", "premise", "premises", "print", "private", "proof",
"section", "set_option", "omit", "classes", "instances", "coercions", "raw", "protected", "qed", "raw", "renaming", "section", "set_option",
"add_rewrite", "extends", "calc", "have", "obtains", "show", "by", "in", "let", "show", "tactic_hint", "take", "then", "universe",
"forall", "fun", "exists", "if", "then", "else", "assume", "match", "universes", "using", "variable", "variables", "with"].join("|")
"take", "obtain", "from", "axioms", "fields"].join("|") );
); );
var storageType = ( var storageType = (
@ -60,9 +61,11 @@ var leanHighlightRules = function() {
var storageModifiers = ( var storageModifiers = (
"\\[(" + "\\[(" +
["persistent", "notation", "parsing-only", "visible", "instance", "class", "prefix", "axioms", "fields", ["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
"multiple-instances", "classes", "instances", "coercions", "options", "trust", "coercions", "declarations", "decls", "instance", "irreducible",
"coercion", "reducible", "irreducible", "raw"].join("|") + "multiple-instances", "notation", "notations", "parsing-only", "persistent",
"reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
].join("|") +
")\\]" ")\\]"
); );