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

Marcus Hirt marcus.hirt at
Thu Nov 22 06:06:19 UTC 2018

I agree. This is too risky this late for 7.0.0 - let’s take the change in 7.1.0. I also agree that   not using the editor font for the value column as a quick fix is a good idea for 7.0.0.

Kind regards,

> On 21 Nov 2018, at 21:42, Elliott Baron <ebaron at> wrote:
> Hi,
>> On 2018-11-20 12:12 p.m., Mario Torre wrote:
>>> 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?
> I have made good progress in allowing the user to resize all fonts used by JMC, but this ends up touching a lot of UI code. There are also still some bugs to resolve with the implementation. I agree with Mario that this is risky to do shortly before release.
> As a quick fix, we could remove or limit the use of the editor font, at least in tables. In the MBean Browser example cited in the bug, I don't see a need to use the editor font for the value column.
> Marcus, what do you think?
> Thanks,
> Elliott
>> Cheers,
>> Mario
>>> 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

More information about the jmc-dev mailing list