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

[Elliott Baron]

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 openjdk.java.net on behalf of ebaron at redhat.com>
>> 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
>>      
>>      
>>
>>