Skip to content

Commit ed04911

Browse files
authored
Properly escape definition names when building search regexes (#1617)
Fixes #1579
1 parent 0c42672 commit ed04911

File tree

3 files changed

+12
-8
lines changed

3 files changed

+12
-8
lines changed

scripts/preprocessor_concepts.py

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,9 +56,10 @@ def make_definition_regex(definition):
5656

5757

5858
def make_loose_definition_regex(definition):
59+
escaped = re.escape(definition)
5960
return re.compile(
60-
definition + r'\s+:(?=[\s({])|' +
61-
r'(?:data|record|infix[lr]?(?:\s+\d+)?)\s+' + definition
61+
escaped + r'\s+:(?=[\s({])|' +
62+
r'(?:data|record|infix[lr]?(?:\s+\d+)?)\s+' + escaped
6263
)
6364

6465

src/complex-numbers/eisenstein-integers.lagda.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,9 +32,10 @@ open import ring-theory.rings
3232

3333
## Idea
3434

35-
The {{#concept "Eisenstein integers" WDID=Q262370 WD="Eisenstein integer"}} are
36-
the [complex numbers](complex-numbers.complex-numbers.md) of the form `a + bω`,
37-
where `ω = -½ + ½√3i`, and where `a` and `b` are
35+
The
36+
{{#concept "Eisenstein integers" WDID=Q262370 WD="Eisenstein integer" Agda=ℤ[ω]}}
37+
are the [complex numbers](complex-numbers.complex-numbers.md) of the form
38+
`a + bω`, where `ω = -½ + ½√3i`, and where `a` and `b` are
3839
[integers](elementary-number-theory.integers.md). Note that `ω` is a solution to
3940
the equation `ω² + ω + 1 = 0`.
4041

src/complex-numbers/gaussian-integers.lagda.md

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -33,9 +33,11 @@ open import ring-theory.rings
3333

3434
## Idea
3535

36-
The {{#concept "Gaussian integers" WDID=Q724975 WD="Gaussian integer"}} are the
37-
[complex numbers](complex-numbers.complex-numbers.md) of the form `a + bi`,
38-
where `a` and `b` are [integers](elementary-number-theory.integers.md).
36+
The
37+
{{#concept "Gaussian integers" WDID=Q724975 WD="Gaussian integer" Agda=ℤ[i]}}
38+
are the [complex numbers](complex-numbers.complex-numbers.md) of the form
39+
`a + bi`, where `a` and `b` are
40+
[integers](elementary-number-theory.integers.md).
3941

4042
## Definition
4143

0 commit comments

Comments
 (0)