Skip to content

Fix Coq-related bug #678 #1648

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Anteru merged 3 commits into from Jan 4, 2021
Merged

Fix Coq-related bug #678 #1648

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a1e8e27
Unicode support for Coq
Dec 25, 2020
2ce788d
Coq lexer: improve `analyse_text`
Dec 25, 2020
02cd333
Add a test for Coq
Dec 28, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions pygments/lexers/theorem.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ class CoqLexer(RegexLexer):
filenames = ['*.v']
mimetypes = ['text/x-coq']

flags = re.UNICODE

keywords1 = (
# Vernacular commands
'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable',
Expand Down Expand Up @@ -123,14 +125,15 @@ class CoqLexer(RegexLexer):
(r'0[bB][01][01_]*', Number.Bin),
(r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),

(r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'",
String.Char),
(r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", String.Char),

(r"'.'", String.Char),
(r"'", Keyword), # a stray quote is another syntax element

(r'"', String.Double, 'string'),

(r'[~?][a-z][\w\']*:', Name),
(r'\S', Name.Builtin.Pseudo),
],
'comment': [
(r'[^(*)]+', Comment),
Expand All @@ -154,7 +157,7 @@ class CoqLexer(RegexLexer):
}

def analyse_text(text):
if 'qed' in text and 'tauto' in text:
if 'Qed' in text and 'Proof' in text:
return 1


Expand Down
33 changes: 33 additions & 0 deletions tests/test_coq.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
# -*- coding: utf-8 -*-
"""
Coq Tests
~~~~~~~~~~~~~
:copyright: Copyright 2006-2020 by the Pygments team, see AUTHORS.
:license: BSD, see LICENSE for details.
"""

import pytest

from pygments.lexers import CoqLexer
from pygments.token import Token

@pytest.fixture(scope='module')
def lexer():
yield CoqLexer()

def test_coq_unicode(lexer):
fragment = 'Check (α ≻ β).\n'
tokens = [
(Token.Keyword.Namespace, 'Check'),
(Token.Text, ' '),
(Token.Operator, '('),
(Token.Name, 'α'),
(Token.Text, ' '),
(Token.Name.Builtin.Pseudo, '≻'),
(Token.Text, ' '),
(Token.Name, 'β'),
(Token.Operator, ')'),
(Token.Operator, '.'),
(Token.Text, '\n'),
]
assert list(lexer.get_tokens(fragment)) == tokens