JMC-6180: Changing the Java source editor font changes the size of some values in the JMC tables
marcus.hirt at oracle.com
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.
> On 21 Nov 2018, at 21:42, Elliott Baron <ebaron at redhat.com> wrote:
>> 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
>>> 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?
>>> Kind regards,
>>> On 2018-11-05, 23:37, "jmc-dev on behalf of Elliott Baron" <
>>> jmc-dev-bounces at openjdk.java.net on behalf of ebaron at redhat.com>
>>> 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
More information about the jmc-dev