-
Notifications
You must be signed in to change notification settings - Fork 743
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.
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
Coq unicode improvements #1764
Coq unicode improvements #1764
Conversation
8f54abd
to
8ff1370
Compare
988c4d6
to
d3db448
Compare
One choice that I made is that the big list of first/second-order logic symbols from the previous effort are now Operator instead of Punctuation. This is basically because most of them are indeed operators. If you want |
I'll push the work anyway, have a look |
This would be very nice to have for Coq projects on gitlab to render better. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot for your contribution @cormacrelf ❤️ Sorry to get back to this PR late 🙏🏼
It looks great to me overall 👍🏼 I have added some suggestions for your consideration. Please let me know what you think.
If possible, could you also rebase this branch of upstream/master
to initiate the CI 🙏🏼?
It would be really good to get this merged. @tancnle can you apply the changes and merge it? |
@gmalecha Sorry for the delay. Let's merge and follow up with some improvement 👍🏼 |
Fixes #1312 for coq.
Unfortunately it does not fix this for every language, but as a general rule for fixing other languages that should support unicode identifiers, replace
[a-z]
/\w
or similar with Ruby's regex unicode classes e.g.\p{L}
for any unicode letter. The Coq version here makes use of\p{S}|\p{Pc}
to cover all symbols and non-parenthetical punctuation, makes them all operators (with some nuances/overrides).