The editor font actually scales now. It didn't before because of multiple reasons:
editor.setFont was called too early. In this state, the editor doesn't have a font applied, so the system default (non-monospaced!) is returned.
This didn't matter though, since editor.setContentType("text/enigma-sources") overwrote it anyway with the DefaultFont property defined in EnigmaSyntaxKit (making the DEFAULT_FONT reflection hack redundant, no idea why that existed).
DefaultFont is usually set to UiConfig.getFallbackEditorFont(), which intends to scale the default monospace font to the current DPI settings.
This didn't work either though, as BasicTweaker#modifyFont only scales UIResources, which Font is not a subclass of.
editor.setFont
was called too early. In this state, the editor doesn't have a font applied, so the system default (non-monospaced!) is returned.editor.setContentType("text/enigma-sources")
overwrote it anyway with theDefaultFont
property defined inEnigmaSyntaxKit
(making theDEFAULT_FONT
reflection hack redundant, no idea why that existed).DefaultFont
is usually set toUiConfig.getFallbackEditorFont()
, which intends to scale the default monospace font to the current DPI settings.BasicTweaker#modifyFont
only scalesUIResource
s, whichFont
is not a subclass of.