eric6/ThirdParty/Pygments/pygments/lexers/tnt.py

changeset 7983
54c5cfbb1e29
parent 7701
25f42e208e08
equal deleted inserted replaced
7982:48d210e41c65 7983:54c5cfbb1e29
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):
53 | axiom\\ ([1-5]) | premise | push | pop 53 | axiom\\ ([1-5]) | premise | push | pop
54 ''') 54 ''')
55 LINENOS = re.compile(r'(?:[0-9]+)(?:(?:, ?|,? and )(?:[0-9]+))*') 55 LINENOS = re.compile(r'(?:[0-9]+)(?:(?:, ?|,? and )(?:[0-9]+))*')
56 COMMENT = re.compile(r'\[[^\n\]]+\]') 56 COMMENT = re.compile(r'\[[^\n\]]+\]')
57 57
58 def __init__(self, *args, **kwargs):
59 Lexer.__init__(self, *args, **kwargs)
60 self.cur = []
61
58 def whitespace(self, start, text, required=False): 62 def whitespace(self, start, text, required=False):
59 """Tokenize whitespace.""" 63 """Tokenize whitespace."""
60 end = start 64 end = start
61 try: 65 try:
62 while text[end] in self.WHITESPACE: 66 while text[end] in self.WHITESPACE:
102 return start+1 106 return start+1
103 raise AssertionError # no matches 107 raise AssertionError # no matches
104 108
105 def formula(self, start, text): 109 def formula(self, start, text):
106 """Tokenize a formula.""" 110 """Tokenize a formula."""
107 if text[start] in '[]': # fantasy push or pop
108 self.cur.append((start, Keyword, text[start]))
109 return start+1
110 if text[start] in self.NEGATORS: # ~<...> 111 if text[start] in self.NEGATORS: # ~<...>
111 end = start+1 112 end = start+1
112 while text[end] in self.NEGATORS: 113 while text[end] in self.NEGATORS:
113 end += 1 114 end += 1
114 self.cur.append((start, Operator, text[start:end])) 115 self.cur.append((start, Operator, text[start:end]))
152 else: 153 else:
153 self.cur.append((start, Keyword, text[start:match.end()])) 154 self.cur.append((start, Keyword, text[start:match.end()]))
154 return match.end() 155 return match.end()
155 156
156 def lineno(self, start, text): 157 def lineno(self, start, text):
157 """Tokenize a line marker.""" 158 """Tokenize a line referral."""
158 end = start 159 end = start
159 while text[end] not in self.NUMBERS: 160 while text[end] not in self.NUMBERS:
160 end += 1 161 end += 1
161 self.cur.append((start, Punctuation, text[start])) 162 self.cur.append((start, Punctuation, text[start]))
162 self.cur.append((start+1, Text, text[start+1:end])) 163 self.cur.append((start+1, Text, text[start+1:end]))
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

eric ide

mercurial