3 pygments.lexers.tnt |
3 pygments.lexers.tnt |
4 ~~~~~~~~~~~~~~~~~~~ |
4 ~~~~~~~~~~~~~~~~~~~ |
5 |
5 |
6 Lexer for Typographic Number Theory. |
6 Lexer for Typographic Number Theory. |
7 |
7 |
8 :copyright: Copyright 2006-2020 by the Pygments team, see AUTHORS. |
8 :copyright: Copyright 2006-2021 by the Pygments team, see AUTHORS. |
9 :license: BSD, see LICENSE for details. |
9 :license: BSD, see LICENSE for details. |
10 """ |
10 """ |
11 |
11 |
12 import re |
12 import re |
13 |
13 |
14 from pygments.lexer import Lexer |
14 from pygments.lexer import Lexer |
15 from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \ |
15 from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \ |
16 Punctuation, Error |
16 Punctuation, Error |
17 |
17 |
18 __all__ = ['TNTLexer'] |
18 __all__ = ['TNTLexer'] |
19 |
19 |
20 |
20 |
21 class TNTLexer(Lexer): |
21 class TNTLexer(Lexer): |
184 def get_tokens_unprocessed(self, text): |
185 def get_tokens_unprocessed(self, text): |
185 """Returns a list of TNT tokens.""" |
186 """Returns a list of TNT tokens.""" |
186 self.cur = [] |
187 self.cur = [] |
187 start = end = self.whitespace(0, text) |
188 start = end = self.whitespace(0, text) |
188 while start <= end < len(text): |
189 while start <= end < len(text): |
189 # try line number |
190 try: |
190 while text[end] in self.NUMBERS: |
191 # try line number |
191 end += 1 |
192 while text[end] in self.NUMBERS: |
192 if end != start: # actual number present |
193 end += 1 |
193 self.cur.append((start, Number.Integer, text[start:end])) |
194 if end != start: # actual number present |
194 # whitespace is required after a line number |
195 self.cur.append((start, Number.Integer, text[start:end])) |
|
196 # whitespace is required after a line number |
|
197 orig = len(self.cur) |
|
198 try: |
|
199 start = end = self.whitespace(end, text, True) |
|
200 except AssertionError: |
|
201 del self.cur[orig:] |
|
202 start = end = self.error_till_line_end(end, text) |
|
203 continue |
|
204 # at this point it could be a comment |
|
205 match = self.COMMENT.match(text, start) |
|
206 if match is not None: |
|
207 self.cur.append((start, Comment, text[start:match.end()])) |
|
208 start = end = match.end() |
|
209 # anything after the closing bracket is invalid |
|
210 start = end = self.error_till_line_end(start, text) |
|
211 # do not attempt to process the rest |
|
212 continue |
|
213 del match |
|
214 if text[start] in '[]': # fantasy push or pop |
|
215 self.cur.append((start, Keyword, text[start])) |
|
216 start += 1 |
|
217 end += 1 |
|
218 else: |
|
219 # one formula, possibly containing subformulae |
|
220 orig = len(self.cur) |
|
221 try: |
|
222 start = end = self.formula(start, text) |
|
223 except AssertionError: # not well-formed |
|
224 del self.cur[orig:] |
|
225 while text[end] not in self.WHITESPACE: |
|
226 end += 1 |
|
227 self.cur.append((start, Error, text[start:end])) |
|
228 start = end |
|
229 # skip whitespace after formula |
195 orig = len(self.cur) |
230 orig = len(self.cur) |
196 try: |
231 try: |
197 start = end = self.whitespace(end, text, True) |
232 start = end = self.whitespace(end, text, True) |
198 except AssertionError: |
233 except AssertionError: |
199 del self.cur[orig:] |
234 del self.cur[orig:] |
200 start = end = self.error_till_line_end(end, text) |
235 start = end = self.error_till_line_end(start, text) |
201 continue |
236 continue |
202 # at this point it could be a comment |
237 # rule proving this formula a theorem |
203 match = self.COMMENT.match(text, start) |
|
204 if match is not None: |
|
205 self.cur.append((start, Comment, text[start:match.end()])) |
|
206 start = end = match.end() |
|
207 # anything after the closing bracket is invalid |
|
208 start = end = self.error_till_line_end(start, text) |
|
209 # do not attempt to process the rest |
|
210 continue |
|
211 del match |
|
212 # one formula, possibly containing subformulae |
|
213 orig = len(self.cur) |
|
214 try: |
|
215 start = end = self.formula(start, text) |
|
216 except AssertionError: # not well-formed |
|
217 del self.cur[orig:] |
|
218 while text[end] not in self.WHITESPACE: |
|
219 end += 1 |
|
220 self.cur.append((start, Error, text[start:end])) |
|
221 start = end |
|
222 # skip whitespace after formula |
|
223 orig = len(self.cur) |
|
224 try: |
|
225 start = end = self.whitespace(end, text, True) |
|
226 except AssertionError: |
|
227 del self.cur[orig:] |
|
228 start = end = self.error_till_line_end(start, text) |
|
229 continue |
|
230 # rule proving this formula a theorem |
|
231 orig = len(self.cur) |
|
232 try: |
|
233 start = end = self.rule(start, text) |
|
234 except AssertionError: |
|
235 del self.cur[orig:] |
|
236 start = end = self.error_till_line_end(start, text) |
|
237 continue |
|
238 # skip whitespace after rule |
|
239 start = end = self.whitespace(end, text) |
|
240 # line marker |
|
241 if text[start] == '(': |
|
242 orig = len(self.cur) |
238 orig = len(self.cur) |
243 try: |
239 try: |
244 start = end = self.lineno(start, text) |
240 start = end = self.rule(start, text) |
245 except AssertionError: |
241 except AssertionError: |
246 del self.cur[orig:] |
242 del self.cur[orig:] |
247 start = end = self.error_till_line_end(start, text) |
243 start = end = self.error_till_line_end(start, text) |
248 continue |
244 continue |
249 start = end = self.whitespace(start, text) |
245 # skip whitespace after rule |
|
246 start = end = self.whitespace(end, text) |
|
247 # line marker |
|
248 if text[start] == '(': |
|
249 orig = len(self.cur) |
|
250 try: |
|
251 start = end = self.lineno(start, text) |
|
252 except AssertionError: |
|
253 del self.cur[orig:] |
|
254 start = end = self.error_till_line_end(start, text) |
|
255 continue |
|
256 start = end = self.whitespace(start, text) |
|
257 except IndexError: |
|
258 try: |
|
259 del self.cur[orig:] |
|
260 except NameError: |
|
261 pass # if orig was never defined, fine |
|
262 self.error_till_line_end(start, text) |
250 return self.cur |
263 return self.cur |