JMC-6180: Changing the Java source editor font changes the size of some values in the JMC tables
ebaron at redhat.com
Wed Nov 21 20:42:48 UTC 2018
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