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

["C. M. Sperberg-McQueen" <cmsmcq@xxxxxxxxxxxxxxxxx>]

Andrew Helwer <andrew.helwer@xxxxxxxxx> writes:

> .... 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: ...
>
> (b)/(c) Pro-remove: ...

I'm not currently a heavy user of TLA+, and I expect the voices of those
who are heavy users should probably weigh more heavily.  But for what
it's worth, the arguments for (a) seem to me much stronger, and to
support (a) as a conclusion.

The arguments brought forward in favor of (b) and (c) are weaker by
nature, and do not in fact support conclusion (b) or (c).  (Some users
use software with disappointing fonts.  Therefore (?!), the software
should forbid other users from using the characters whose rendering is
thought to be poor, or perhaps the parser and the standard should just
be brought out of alignment with each other.)  The idea that
semantically precise Unicode encodings of operators should be eliminated
in favor of less precise ASCII encodings would be a hard one to sell me,
even if the primary argument in its favor were stronger than the
observation that some users don't think highly of some Unicode fonts.

That's my two cents (Use only as directed, void where prohibited by law,
past performance is not a guarantee of future results, if condition
persists consult a qualified font designer).

-- 
C. M. Sperberg-McQueen
Black Mesa Technologies LLC
http://blackmesatech.com

-- 
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/87wmmsijxq.fsf%40blackmesatech.com.