Skip to content

Commit

Permalink
Add support for escaping EOL in string literals
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Dec 30, 2023
1 parent ea8440e commit 843b426
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 2 deletions.
2 changes: 1 addition & 1 deletion pygments/lexers/lean.py
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ class Lean4Lexer(RegexLexer):
],
'string': [
(r'[^\\"]+', String.Double),
(r'\\[n"\\]', String.Escape),
(r'\\[n"\\\n]', String.Escape),
('"', String.Double, '#pop'),
],
}
Expand Down
4 changes: 4 additions & 0 deletions tests/examplefiles/lean4/Test.lean
Original file line number Diff line number Diff line change
Expand Up @@ -238,3 +238,7 @@ variable {ι A B : Type*} (𝒜 : ι → A) (ℬ : ι → B)
#check `𝒜.a
#check ``𝒜
#check "\
This is\na \
wrapped string.
15 changes: 14 additions & 1 deletion tests/examplefiles/lean4/Test.lean.output

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit 843b426

Please sign in to comment.