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

Mario Torre neugens at
Tue Nov 20 17:12:49 UTC 2018

On Tue, 2018-11-06 at 15:06 +0100, Marcus Hirt wrote:
> 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.

I'm a bit concerned by the scope of this, do you think it would make
more sense to approach the patch incrementally?

>From what I gather this is quite a massive patch I'm not sure we want
that in before release.

Any suggestions?


> Kind regards,
> Marcus
> On 2018-11-05, 23:37, "jmc-dev on behalf of Elliott Baron" <
> jmc-dev-bounces at on behalf of ebaron at>
> wrote:
>     Hi,
>     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?
>     Thanks,
>     Elliott
Mario Torre
Associate Manager, Software Engineering
Red Hat GmbH <>
9704 A60C B4BE A8B8 0F30  9205 5D7E 4952 3F65 7898

More information about the jmc-dev mailing list