blog/root/js/ace-editor/src-noconflict/mode-lean.js

282 lines
9.5 KiB
JavaScript
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

ace.define("ace/mode/doc_comment_highlight_rules",["require","exports","module","ace/lib/oop","ace/mode/text_highlight_rules"], function(require, exports, module) {
"use strict";
var oop = require("../lib/oop");
var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
var DocCommentHighlightRules = function() {
this.$rules = {
"start" : [ {
token : "comment.doc.tag",
regex : "@[\\w\\d_]+" // TODO: fix email addresses
},
DocCommentHighlightRules.getTagRule(),
{
defaultToken : "comment.doc",
caseInsensitive: true
}]
};
};
oop.inherits(DocCommentHighlightRules, TextHighlightRules);
DocCommentHighlightRules.getTagRule = function(start) {
return {
token : "comment.doc.tag.storage.type",
regex : "\\b(?:TODO|FIXME|XXX|HACK)\\b"
};
}
DocCommentHighlightRules.getStartRule = function(start) {
return {
token : "comment.doc", // doc comment
regex : "\\/\\*(?=\\*)",
next : start
};
};
DocCommentHighlightRules.getEndRule = function (start) {
return {
token : "comment.doc", // closing comment
regex : "\\*\\/",
next : start
};
};
exports.DocCommentHighlightRules = DocCommentHighlightRules;
});
ace.define("ace/mode/lean_highlight_rules",["require","exports","module","ace/lib/oop","ace/mode/doc_comment_highlight_rules","ace/mode/text_highlight_rules"], function(require, exports, module) {
"use strict";
var oop = require("../lib/oop");
var DocCommentHighlightRules = require("./doc_comment_highlight_rules").DocCommentHighlightRules;
var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
var leanHighlightRules = function() {
var keywordControls = (
[ "add_rewrite", "alias", "as", "assume", "attribute",
"begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
"classes", "coercions", "conjecture", "constants", "context",
"corollary", "else", "end", "environment", "eval", "example",
"exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
"forall", "from", "fun", "have", "help", "hiding", "if",
"import", "in", "infix", "infixl", "infixr", "instances",
"let", "local", "match", "namespace", "notation", "obtain", "obtains",
"omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
"precedence", "prefix", "premise", "premises", "print", "private", "proof",
"protected", "qed", "raw", "renaming", "section", "set_option",
"show", "tactic_hint", "take", "then", "universe",
"universes", "using", "variable", "variables", "with"].join("|")
);
var nameProviders = (
["inductive", "structure", "record", "theorem", "axiom",
"axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
);
var storageType = (
["Prop", "Type", "Type'", "Type₊", "Type₁", "Type₂", "Type₃"].join("|")
);
var storageModifiers = (
"\\[(" +
["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
"coercions", "declarations", "decls", "instance", "irreducible",
"multiple-instances", "notation", "notations", "parsing-only", "persistent",
"reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
].join("|") +
")\\]"
);
var keywordOperators = (
[].join("|")
);
var keywordMapper = this.$keywords = this.createKeywordMapper({
"keyword.control" : keywordControls,
"storage.type" : storageType,
"keyword.operator" : keywordOperators,
"variable.language": "sorry"
}, "identifier");
var identifierRe = "[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z0-9_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*";
var operatorRe = new RegExp(["#", "@", "->", "", "↔", "/", "==", "=", ":=", "<->",
"/\\", "\\/", "∧", "", "≠", "<", ">", "≤", "≥", "¬",
"<=", ">=", "⁻¹", "⬝", "▸", "\\+", "\\*", "-", "/",
"λ", "→", "∃", "∀", ":="].join("|"));
this.$rules = {
"start" : [
{
token : "comment", // single line comment "--"
regex : "--.*$"
},
DocCommentHighlightRules.getStartRule("doc-start"),
{
token : "comment", // multi line comment "/-"
regex : "\\/-",
next : "comment"
}, {
stateName: "qqstring",
token : "string.start", regex : '"', next : [
{token : "string.end", regex : '"', next : "start"},
{token : "constant.language.escape", regex : /\\[n"\\]/},
{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"
}, {
token : "constant.numeric", // float
regex : "[+-]?\\d+(?:(?:\\.\\d*)?(?:[eE][+-]?\\d+)?)?(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
}, {
token : "storage.modifier",
regex : storageModifiers
}, {
token : keywordMapper,
regex : identifierRe
}, {
token : "operator",
regex : operatorRe
}, {
token : "punctuation.operator",
regex : "\\?|\\:|\\,|\\;|\\."
}, {
token : "paren.lparen",
regex : "[[({]"
}, {
token : "paren.rparen",
regex : "[\\])}]"
}, {
token : "text",
regex : "\\s+"
}
],
"comment" : [ {token: "comment", regex: "-/", next: "start"},
{defaultToken: "comment"} ]
};
this.embedRules(DocCommentHighlightRules, "doc-",
[ DocCommentHighlightRules.getEndRule("start") ]);
this.normalizeRules();
};
oop.inherits(leanHighlightRules, TextHighlightRules);
exports.leanHighlightRules = leanHighlightRules;
});
ace.define("ace/mode/matching_brace_outdent",["require","exports","module","ace/range"], function(require, exports, module) {
"use strict";
var Range = require("../range").Range;
var MatchingBraceOutdent = function() {};
(function() {
this.checkOutdent = function(line, input) {
if (! /^\s+$/.test(line))
return false;
return /^\s*\}/.test(input);
};
this.autoOutdent = function(doc, row) {
var line = doc.getLine(row);
var match = line.match(/^(\s*\})/);
if (!match) return 0;
var column = match[1].length;
var openBracePos = doc.findMatchingBracket({row: row, column: column});
if (!openBracePos || openBracePos.row == row) return 0;
var indent = this.$getIndent(doc.getLine(openBracePos.row));
doc.replace(new Range(row, 0, row, column-1), indent);
};
this.$getIndent = function(line) {
return line.match(/^\s*/)[0];
};
}).call(MatchingBraceOutdent.prototype);
exports.MatchingBraceOutdent = MatchingBraceOutdent;
});
ace.define("ace/mode/lean",["require","exports","module","ace/lib/oop","ace/mode/text","ace/mode/lean_highlight_rules","ace/mode/matching_brace_outdent","ace/range"], function(require, exports, module) {
"use strict";
var oop = require("../lib/oop");
var TextMode = require("./text").Mode;
var leanHighlightRules = require("./lean_highlight_rules").leanHighlightRules;
var MatchingBraceOutdent = require("./matching_brace_outdent").MatchingBraceOutdent;
var Range = require("../range").Range;
var Mode = function() {
this.HighlightRules = leanHighlightRules;
this.$outdent = new MatchingBraceOutdent();
};
oop.inherits(Mode, TextMode);
(function() {
this.lineCommentStart = "--";
this.blockComment = {start: "/-", end: "-/"};
this.getNextLineIndent = function(state, line, tab) {
var indent = this.$getIndent(line);
var tokenizedLine = this.getTokenizer().getLineTokens(line, state);
var tokens = tokenizedLine.tokens;
var endState = tokenizedLine.state;
if (tokens.length && tokens[tokens.length-1].type == "comment") {
return indent;
}
if (state == "start") {
var match = line.match(/^.*[\{\(\[]\s*$/);
if (match) {
indent += tab;
}
} else if (state == "doc-start") {
if (endState == "start") {
return "";
}
var match = line.match(/^\s*(\/?)\*/);
if (match) {
if (match[1]) {
indent += " ";
}
indent += "- ";
}
}
return indent;
};
this.checkOutdent = function(state, line, input) {
return this.$outdent.checkOutdent(line, input);
};
this.autoOutdent = function(state, doc, row) {
this.$outdent.autoOutdent(doc, row);
};
this.$id = "ace/mode/lean";
}).call(Mode.prototype);
exports.Mode = Mode;
});