corrade-nucleus-nucleons – Blame information for rev 20

Subversion Repositories:
Rev:
Rev Author Line No. Line
20 office 1 define("ace/mode/doc_comment_highlight_rules",["require","exports","module","ace/lib/oop","ace/mode/text_highlight_rules"], function(require, exports, module) {
2 "use strict";
3  
4 var oop = require("../lib/oop");
5 var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
6  
7 var DocCommentHighlightRules = function() {
8 this.$rules = {
9 "start" : [ {
10 token : "comment.doc.tag",
11 regex : "@[\\w\\d_]+" // TODO: fix email addresses
12 },
13 DocCommentHighlightRules.getTagRule(),
14 {
15 defaultToken : "comment.doc",
16 caseInsensitive: true
17 }]
18 };
19 };
20  
21 oop.inherits(DocCommentHighlightRules, TextHighlightRules);
22  
23 DocCommentHighlightRules.getTagRule = function(start) {
24 return {
25 token : "comment.doc.tag.storage.type",
26 regex : "\\b(?:TODO|FIXME|XXX|HACK)\\b"
27 };
28 }
29  
30 DocCommentHighlightRules.getStartRule = function(start) {
31 return {
32 token : "comment.doc", // doc comment
33 regex : "\\/\\*(?=\\*)",
34 next : start
35 };
36 };
37  
38 DocCommentHighlightRules.getEndRule = function (start) {
39 return {
40 token : "comment.doc", // closing comment
41 regex : "\\*\\/",
42 next : start
43 };
44 };
45  
46  
47 exports.DocCommentHighlightRules = DocCommentHighlightRules;
48  
49 });
50  
51 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) {
52 "use strict";
53  
54 var oop = require("../lib/oop");
55 var DocCommentHighlightRules = require("./doc_comment_highlight_rules").DocCommentHighlightRules;
56 var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
57  
58 var leanHighlightRules = function() {
59  
60 var keywordControls = (
61 [ "add_rewrite", "alias", "as", "assume", "attribute",
62 "begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
63 "classes", "coercions", "conjecture", "constants", "context",
64 "corollary", "else", "end", "environment", "eval", "example",
65 "exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
66 "forall", "from", "fun", "have", "help", "hiding", "if",
67 "import", "in", "infix", "infixl", "infixr", "instances",
68 "let", "local", "match", "namespace", "notation", "obtain", "obtains",
69 "omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
70 "precedence", "prefix", "premise", "premises", "print", "private", "proof",
71 "protected", "qed", "raw", "renaming", "section", "set_option",
72 "show", "tactic_hint", "take", "then", "universe",
73 "universes", "using", "variable", "variables", "with"].join("|")
74 );
75  
76 var nameProviders = (
77 ["inductive", "structure", "record", "theorem", "axiom",
78 "axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
79 );
80  
81 var storageType = (
82 ["Prop", "Type", "Type'", "Type₊", "Type₁", "Type₂", "Type₃"].join("|")
83 );
84  
85 var storageModifiers = (
86 "\\[(" +
87 ["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
88 "coercions", "declarations", "decls", "instance", "irreducible",
89 "multiple-instances", "notation", "notations", "parsing-only", "persistent",
90 "reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
91 ].join("|") +
92 ")\\]"
93 );
94  
95 var keywordOperators = (
96 [].join("|")
97 );
98  
99 var keywordMapper = this.$keywords = this.createKeywordMapper({
100 "keyword.control" : keywordControls,
101 "storage.type" : storageType,
102 "keyword.operator" : keywordOperators,
103 "variable.language": "sorry"
104 }, "identifier");
105  
106 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]*";
107 var operatorRe = new RegExp(["#", "@", "->", "∼", "↔", "/", "==", "=", ":=", "<->",
108 "/\\", "\\/", "∧", "∨", "≠", "<", ">", "≤", "≥", "¬",
109 "<=", ">=", "⁻¹", "⬝", "▸", "\\+", "\\*", "-", "/",
110 "λ", "→", "∃", "∀", ":="].join("|"));
111  
112 this.$rules = {
113 "start" : [
114 {
115 token : "comment", // single line comment "--"
116 regex : "--.*$"
117 },
118 DocCommentHighlightRules.getStartRule("doc-start"),
119 {
120 token : "comment", // multi line comment "/-"
121 regex : "\\/-",
122 next : "comment"
123 }, {
124 stateName: "qqstring",
125 token : "string.start", regex : '"', next : [
126 {token : "string.end", regex : '"', next : "start"},
127 {token : "constant.language.escape", regex : /\\[n"\\]/},
128 {defaultToken: "string"}
129 ]
130 }, {
131 token : "keyword.control", regex : nameProviders, next : [
132 {token : "variable.language", regex : identifierRe, next : "start"} ]
133 }, {
134 token : "constant.numeric", // hex
135 regex : "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
136 }, {
137 token : "constant.numeric", // float
138 regex : "[+-]?\\d+(?:(?:\\.\\d*)?(?:[eE][+-]?\\d+)?)?(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
139 }, {
140 token : "storage.modifier",
141 regex : storageModifiers
142 }, {
143 token : keywordMapper,
144 regex : identifierRe
145 }, {
146 token : "operator",
147 regex : operatorRe
148 }, {
149 token : "punctuation.operator",
150 regex : "\\?|\\:|\\,|\\;|\\."
151 }, {
152 token : "paren.lparen",
153 regex : "[[({]"
154 }, {
155 token : "paren.rparen",
156 regex : "[\\])}]"
157 }, {
158 token : "text",
159 regex : "\\s+"
160 }
161 ],
162 "comment" : [ {token: "comment", regex: "-/", next: "start"},
163 {defaultToken: "comment"} ]
164 };
165  
166 this.embedRules(DocCommentHighlightRules, "doc-",
167 [ DocCommentHighlightRules.getEndRule("start") ]);
168 this.normalizeRules();
169 };
170  
171 oop.inherits(leanHighlightRules, TextHighlightRules);
172  
173 exports.leanHighlightRules = leanHighlightRules;
174 });
175  
176 define("ace/mode/matching_brace_outdent",["require","exports","module","ace/range"], function(require, exports, module) {
177 "use strict";
178  
179 var Range = require("../range").Range;
180  
181 var MatchingBraceOutdent = function() {};
182  
183 (function() {
184  
185 this.checkOutdent = function(line, input) {
186 if (! /^\s+$/.test(line))
187 return false;
188  
189 return /^\s*\}/.test(input);
190 };
191  
192 this.autoOutdent = function(doc, row) {
193 var line = doc.getLine(row);
194 var match = line.match(/^(\s*\})/);
195  
196 if (!match) return 0;
197  
198 var column = match[1].length;
199 var openBracePos = doc.findMatchingBracket({row: row, column: column});
200  
201 if (!openBracePos || openBracePos.row == row) return 0;
202  
203 var indent = this.$getIndent(doc.getLine(openBracePos.row));
204 doc.replace(new Range(row, 0, row, column-1), indent);
205 };
206  
207 this.$getIndent = function(line) {
208 return line.match(/^\s*/)[0];
209 };
210  
211 }).call(MatchingBraceOutdent.prototype);
212  
213 exports.MatchingBraceOutdent = MatchingBraceOutdent;
214 });
215  
216 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) {
217 "use strict";
218  
219 var oop = require("../lib/oop");
220 var TextMode = require("./text").Mode;
221 var leanHighlightRules = require("./lean_highlight_rules").leanHighlightRules;
222 var MatchingBraceOutdent = require("./matching_brace_outdent").MatchingBraceOutdent;
223 var Range = require("../range").Range;
224  
225 var Mode = function() {
226 this.HighlightRules = leanHighlightRules;
227  
228 this.$outdent = new MatchingBraceOutdent();
229 };
230 oop.inherits(Mode, TextMode);
231  
232 (function() {
233  
234 this.lineCommentStart = "--";
235 this.blockComment = {start: "/-", end: "-/"};
236  
237 this.getNextLineIndent = function(state, line, tab) {
238 var indent = this.$getIndent(line);
239  
240 var tokenizedLine = this.getTokenizer().getLineTokens(line, state);
241 var tokens = tokenizedLine.tokens;
242 var endState = tokenizedLine.state;
243  
244 if (tokens.length && tokens[tokens.length-1].type == "comment") {
245 return indent;
246 }
247  
248 if (state == "start") {
249 var match = line.match(/^.*[\{\(\[]\s*$/);
250 if (match) {
251 indent += tab;
252 }
253 } else if (state == "doc-start") {
254 if (endState == "start") {
255 return "";
256 }
257 var match = line.match(/^\s*(\/?)\*/);
258 if (match) {
259 if (match[1]) {
260 indent += " ";
261 }
262 indent += "- ";
263 }
264 }
265  
266 return indent;
267 };
268  
269 this.checkOutdent = function(state, line, input) {
270 return this.$outdent.checkOutdent(line, input);
271 };
272  
273 this.autoOutdent = function(state, doc, row) {
274 this.$outdent.autoOutdent(doc, row);
275 };
276  
277 this.$id = "ace/mode/lean";
278 }).call(Mode.prototype);
279  
280 exports.Mode = Mode;
281 });