rouge-ruby
Coq unicode improvements
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).
There's even a little nuance that's hard to see in the Github theme, which you get back with monokai etc
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 +-* (from the bullet point goal selection syntax) to be Punctuation like all the braces are, then the way to go is differentiating between proof mode sentence-initial symbols (ie bullets) and symbols anywhere else. You can push/pop proof mode with Proof. and Qed. (et al). It works but is obviously going to be slightly more fragile to invalid syntax.
This would be very nice to have for Coq projects on gitlab to render better.
It would be really good to get this merged. @tancnle can you apply the changes and merge it?
It would be really good to get this merged. @tancnle can you apply the changes and merge it?
👋🏼 @gmalecha I can go over the PR again and apply these changes.
Thank you so much @tancnle!
Who can approve to merge? I have another PR that I'd also like to merge related to Coq string parsing (#1116).
@gmalecha Sorry for the delay. Let's merge and follow up with some improvement 👍🏼