DejaVu Mono is a fixed-width TTF font that seems like it has all the necessary glyphs (see page 26 of
this document), it is free, and while the Toolbox uses SWT and I don't know how that toolkit renders fonts, I see no reason why it shouldn't be possible.
Ron
On Monday, March 28, 2016 at 6:45:44 PM UTC+3, Leslie Lamport wrote:
Hi Ron,
There is one potential problem that would make a Unicode version of TLA+ impossible: because of TLA+'s use of indentation, it would require a fixed-width Unicode font. So I suggest that you investigate whether one exists and can be used by ordinary Java programs. If it does, then this would not be too hard to implement, and I would be happy to help a volunteer do it.
Leslie