JMC-6180: Changing the Java source editor font changes the size of some values in the JMC tables

Marcus Hirt marcus.hirt at
Tue Nov 6 14:06:32 UTC 2018

Hi Elliott,

Yes, I _think_ that would be the expected behavior from a user's perspective. 
If anyone thinks differently, please let me know and we can discuss the pros
and cons.

Kind regards,

On 2018-11-05, 23:37, "jmc-dev on behalf of Elliott Baron" <jmc-dev-bounces at on behalf of ebaron at> wrote:

    I'm working on a solution to this bug that allows the user to scale the 
    font size used by JMC labels using the same shortcuts as Eclipse's text 
    editor zoom-in/out functionality (which also simply scale the font size).
    Just to be clear, this functionality should scale font sizes for all JMC 
    editors and views, and not just those using the Eclipse editor font?

More information about the jmc-dev mailing list