lean: fix the name regex by eric-wieser · Pull Request #2614 · pygments/pygments
Navigation Menu
{{ message }}
- Notifications You must be signed in to change notification settings
- Fork 781
Merged
Anteru merged 4 commits intopygments:masterfrom
Dec 30, 2023Merged
Anteru merged 4 commits intopygments:masterfrom
Anteru merged 4 commits intopygments:masterfrom
Conversation
Copy link
Contributor
eric-wieser
commented
Dec 23, 2023
eric-wieser
commented
This corrects it to include the full range of unicode characters that are legal.
This also takes the opportunity to add support for highlighting `name and ``checked_name literals.
eric-wieser added 4 commits
December 23, 2023 16:05This corrects it to include the full range of unicode characters that are legal
eric-wieser commented Dec 23, 2023
|
|
||
| variables {ι A B : Type*} (𝒜 : ι → A) (ℬ : ι → B) | ||
|
|
||
| #check `𝒜.a |
Copy link
Contributor Author
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is mis-highlighted by github, the .a is part of the symbol too!
Anteru
added
changelog-update
labels
Dec 30, 2023
Copy link
Collaborator
Anteru
commented
Dec 30, 2023
Anteru commented
Dec 30, 2023Merged, thanks. My Unicode skills aren't good enough to understand whether the ranges map but I presume you know what you're doing there :)
Anteru
merged commit
4269c7e
into
pygments:master
Anteru
added this to the
2.18.0 milestone
Anteru
removed
the
changelog-update
label
Dec 30, 2023This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment