asai
asai copied to clipboard
RedPRL
Configurable unicode
In my experience so far, I've found that most of my users do not have a font installed that can display the "halfwidth rightwards arrow" character ï¿«, with the result that the error messages look kind of ugly. It would be nice if I could tell Asai to use a different character there, so that I wouldn't have to ask people to install new fonts just to make error messages look nice.
That's a reasonable ask!
Just to confirm, this is only for Asai's diagnostic chrome, and not for unicode that appears in programmer supplied messages?
Yeah, I wouldn't expect Asai to munge messages supplied by the programmer. That's their own lookout. Basically I want to be able to change this line:
https://github.com/RedPRL/asai/blob/main/src/tty/Tty.ml#L66
I don't know if it's worth letting the programmer customize it entirely. Perhaps there could just be three possible settings: the rare unicode character ï¿«, some more common unicode character, and an ascii character or sequence. Or just two of them.
One might argue that the indent_decorations should also be configurable. I haven't noticed a problem with those, but maybe that's because I'm not using backtraces much in userspace. As long as you're making the change, you could maybe give another option for those too.
I think a pure ASCII backend is probably the move instead of offering per-character settings. I'll take a look at this later today