Skip to content

Commit

Permalink
pygments: Strip error tokens from output of provers other than Coq
Browse files Browse the repository at this point in the history
  • Loading branch information
cpitclaudel committed Aug 27, 2021
1 parent 622fa8e commit 2105b12
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion alectryon/pygments.py
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
import pygments
import pygments.styles
import pygments.formatters
from pygments.token import Error, STANDARD_TYPES, Name, Operator
from pygments.token import Error, STANDARD_TYPES, Name, Operator, Text
from pygments.filters import Filter, TokenMergeFilter, NameHighlightFilter
from pygments.formatter import Formatter
from pygments.lexers import get_lexer_by_name # pylint: disable=no-name-in-module
Expand Down Expand Up @@ -58,6 +58,7 @@ def get_lexer(lang):
lexer.add_filter(WarnOnErrorTokenFilter())
else:
lexer = get_lexer_by_name(lang, ensurenl=False)
lexer.add_filter(StripErrorsTokenFilter())
lexer.add_filter(TokenMergeFilter())
return lexer

Expand Down Expand Up @@ -236,6 +237,15 @@ def filter(self, _lexer, stream):
warnings.warn(MSG.format(val, indent(context, ' ' * 8)))
yield typ, val

class StripErrorsTokenFilter(Filter):
"""Change ``Error`` tokens to ``Text`` ones."""

def filter(self, _lexer, stream):
for typ, val in stream:
if typ is Error:
typ = Text
yield typ, val

def replace_builtin_coq_lexer():
"""Monkey-patch pygments to replace the built-in Coq Lexer.
Expand Down

0 comments on commit 2105b12

Please sign in to comment.