corrade-nucleus-nucleons – Blame information for rev 24
?pathlinks?
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 | }); |