[BLUEJ-1250] Include a font fallback for the editor and terminal
In the editor and terminal, we have CSS to explicitly set the -fx-font-family to a specified editor font, which is Roboto Mono. (See PrefMgr.getEditorFontCSS and its callers.) But Roboto Mono has a relatively small set of characters, so if the character is not included, JavaFX will fall back to a different font to display these characters. This is reasonable, except that the font may not be monospace, which means that non-English characters (a user was using box-drawing characters, but this also may apply to things like Arabic or Chinese text) may appear non-monospace in an otherwise monospace display, which can look weird. We should probably specify a monospace fallback font using the usual CSS mechanisms for this.
Issue metadata
- Issue type: Bug
- Priority: Medium