Skip to content

Commit

Permalink
Add the analyze_text method
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Dec 30, 2023
1 parent d0e9946 commit e0e4be3
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 0 deletions.
9 changes: 9 additions & 0 deletions pygments/lexers/lean.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
:copyright: Copyright 2006-2023 by the Pygments team, see AUTHORS.
:license: BSD, see LICENSE for details.
"""
import re

from pygments.lexer import RegexLexer, words, include
from pygments.token import Comment, Operator, Keyword, Name, String, \
Expand Down Expand Up @@ -122,6 +123,10 @@ class Lean3Lexer(RegexLexer):
],
}

def analyse_text(text):
if re.search(r'^import [a-z]', text, re.MULTILINE):
return 0.1


LeanLexer = Lean3Lexer

Expand Down Expand Up @@ -222,3 +227,7 @@ class Lean4Lexer(RegexLexer):
('"', String.Double, '#pop'),
],
}

def analyse_text(text):
if re.search(r'^import [A-Z]', text, re.MULTILINE):
return 0.1
24 changes: 24 additions & 0 deletions tests/test_theorem.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
import textwrap
import pytest

from pygments.lexers.lean import Lean3Lexer, Lean4Lexer

def test_lean3_import():
s = textwrap.dedent("""\
-- this is Lean 3
import data.nat.basic
def foo : nat := 1
""")
assert Lean3Lexer.analyse_text(s) > 0
assert Lean4Lexer.analyse_text(s) == 0

def test_lean4_import():
s = textwrap.dedent("""\
-- this is Lean 4
import Mathlib.Data.Nat.Basic
def foo : Nat := 1
""")
assert Lean3Lexer.analyse_text(s) == 0
assert Lean4Lexer.analyse_text(s) > 0

0 comments on commit e0e4be3

Please sign in to comment.