-
-
Notifications
You must be signed in to change notification settings - Fork 187
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
Support Unicode in pcal.trans
#911
base: master
Are you sure you want to change the base?
Conversation
215d8b0
to
00aaf05
Compare
@lemmy this workflow run is in an infinite loop btw; cancel if you have time! https://github.com/tlaplus/tlaplus/actions/runs/8713343718 |
@lemmy you canceled the wrong run! |
2bf6b9a
to
1fe58f2
Compare
6a79c3f
to
31dfcaa
Compare
Presumably, you can add a |
@Calvin-L it seems all discussions are resolved and it's been approved. Can this perhaps be merged? |
@lemmy I'd like to get this PR merged; it looks like this is starting to affect users who are excited about unicode support. Are you planning to review this one or should I go ahead and merge it? |
I left two review comments above. |
They may have been lost; I don't see them :( |
@@ -1440,7 +1442,7 @@ public static AST.SingleAssign GetSingleAssign() throws ParseAlgorithmException | |||
* PeekAtAlgToken(1), so LAT[0] contains the next token. * | |||
******************************************************************/ | |||
result.lhs = GetLhs() ; | |||
GobbleThis(":=") ; | |||
GobbleThis(":=", "≔") ; |
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.
For me here on Github, ≔ only becomes discernible at zoom levels above 150%. How is ≔ rendered in relation to the other symbols in the different TLA+ IDEs?
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.
How is ≔ rendered in relation to the other symbols in the different TLA+ IDEs?
Well, here's what it looks like in Emacs
For me here on Github, ≔ only becomes discernible at zoom levels above 150%.
I think it depends. I can clearly see right here in your comment the ≔
symbol without having to zoom in.
As a matter of fact, my native language has a symbol such as ё
which you'd probably consider even worse. But I assure you we have no problem with that symbol 😊
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.
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.
It's good to know that Emacs uses a sensible symbol. However, since most TLA+ users use the Toolbox or the VSCode extension, this is where we need to ensure it renders correctly/decently out of the box.
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.
since most TLA+ users use the Toolbox or the VSCode extension
Yeah, I confirm the character looks terrible in VScode and reordering fonts to render emoji with a different one simply doesn't work for some reason.
Anyway, it is a font problem.
this is where we need to ensure it renders correctly/decently out of the box
It's impossible. I mean, tla+toolbox kind of can try to set up fonts in such a way so this emoji renders correctly, but in the end you can't guarantee the font won't be missing on the end-user's system. Not to mention, for external editors such as VSCode you can't do anything at all.
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.
Yeah, I confirm the character looks terrible in VScode and reordering fonts to render emoji with a different one simply doesn't work for some reason.
Anyway, it is a font problem.
this is where we need to ensure it renders correctly/decently out of the box
It's impossible. I mean, tla+toolbox kind of can try to set up fonts in such a way so this emoji renders correctly, but in the end you can't guarantee the font won't be missing on the end-user's system. Not to mention, for external editors such as VSCode you can't do anything at all.
Primarily, it is our problem if the user experience is poor. Declaring it impossible to improve is not acceptable. If a good user experience cannot be provided out of the box, we need to at least provide documentation to guide users on how to fix it.
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.
After discussion in the monthly community meeting this morning I have opened a discussion in the google group about this: https://groups.google.com/g/tlaplus/c/P-GLlN07ARo/m/I5hGjR6AFAAJ
I guess I just learned that "Pending" doesn't mean that a review comment is pending resolution, but that it is invisible to everybody but me. %-) |
Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
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.
I will approve this PR, but we need to ensure that the user experience with the main TLA+ IDEs is ready before we advertise Unicode support.
All right sounds good, that sort of announcement can come whenever we add the Nat/Int/Real unicode definitions to the standard modules. Seems like Calvin already also approved these changes so they seem good to merge. |
These changes build on top of #909. They make the PlusCal translator correctly parse Unicode input. However, it will still always output generated TLA+ code in ASCII.
For testing, all PlusCal modules in the tlaplus/examples repo are converted to Unicode then translated.
Closes #928