[tlaplus] Seeking community feedback: keep or remove some Unicode symbols?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Here is the list of Unicode symbols that are currently supported by SANY: https://github.com/tlaplus/tlaplus-standard/blob/main/unicode/tla-unicode.csv

The symbols under discussion very closely resemble their ASCII counterparts, and are as follows (name, ASCII, Unicode):

• label_as, ::, ∷
• assign, :=, ≔
• bnf_rule, ::=, ⩴
• dots_2, .., ‥
• dots_3, ..., …
• vertver, ||, ‖
• excl, !!, ‼
• qq, ??, ⁇

At the monthly community meeting this morning we discussed how some Unicode symbols do not render very well across several fonts such as those used in GitHub, VS Code, and the Toolbox. The assign and bnf_rule symbols are especially bad. Here is the PR which precipitated this discussion. I am seeking peoples' feedback on whether these Unicode symbols should be (a) kept, (b) removed from the standard but accepted by the parser, or (c) both removed from the standard and rejected by the parser. I will summarize the arguments as:

(a) Pro-keep: this is fundamentally a client font issue; examples exist where these symbols are rendered nicely. As Unicode support grows across fonts, font designers will put more effort into ensuring a wider array of symbols are rendered pleasingly. Furthermore, parser support for these symbols simply offers people a choice to use them; if they wish to use the ASCII equivalents that will always be available to them.

(b)/(c) Pro-remove: at the moment these symbols do not provide a good user experience in the event that they are using Unicode specs in the Toolbox, VS Code, or GitHub (note: neither the Toolbox nor VS Code extension currently have a functioning as-you-type Unicode translator extension). Furthermore, the symbols under discussion do not meaningfully improve the presentation over their ASCII equivalents; they simply resemble contracted forms of the ASCII code string.

Look forward to your thoughts!

Andrew Helwer

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0d7134bb-a9e5-4449-af09-72e768c45e0en%40googlegroups.com.