Configurable unicode

[mikeshulman]

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.

[TOTBWF]

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?

[mikeshulman]

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.

[TOTBWF]

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