Skip to content
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

𝟎-𝟗 and 𝟘-𝟡 Identifiers #32838

Merged
merged 4 commits into from
Aug 12, 2019

Conversation

ajozefiak
Copy link
Contributor

Implementation of issue #26808

Copy link
Member

@StefanKarpinski StefanKarpinski left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this allow all bold and double struck digits, not just 0s and 1s?

@StefanKarpinski
Copy link
Member

In fact, looking at this page, maybe all of U+1d7ce through U+1D7FF. It seems like the same reasoning applies to all of these if it applies to any of them. Although maybe not the sans-serif and monospace digits since those are pretty likely to just look like normal digits in many places, as opposed to the bold and double struck ones, which are a common typographical convention.

@Keno
Copy link
Member

Keno commented Aug 9, 2019

The consistent thing to do would be to allow all of ND expect ASCII 0-9

@StefanKarpinski
Copy link
Member

Consistent, sure, but we might want to normalize some of them first.

@Keno
Copy link
Member

Keno commented Aug 9, 2019

Sure, but that's a) an orthogonal concern and b), breaking since we already allow these in identifiers (just not in leading position).

@JeffBezanson
Copy link
Member

I vote for adding U+1d7ce through U+1d7e1

@Keno
Copy link
Member

Keno commented Aug 9, 2019

Works for me. We can always add more of Nd later if we want.

@ajozefiak ajozefiak changed the title 𝟏, 𝟎, 𝟙, 𝟘 Identifiers 𝟏-𝟗 and 𝟘-𝟡 Identifiers Aug 9, 2019
@ajozefiak ajozefiak changed the title 𝟏-𝟗 and 𝟘-𝟡 Identifiers 𝟎-𝟗 and 𝟘-𝟡 Identifiers Aug 9, 2019
@JeffBezanson JeffBezanson added the needs news A NEWS entry is required for this change label Aug 10, 2019
@JeffBezanson
Copy link
Member

A NEWS entry would be good.

@mbauman mbauman removed the needs news A NEWS entry is required for this change label Aug 12, 2019
@JeffBezanson JeffBezanson merged commit 79ea337 into JuliaLang:master Aug 12, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants