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

[Mario Torre]

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?

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
>     
>     
> 
> 
-- 
Mario Torre
Associate Manager, Software Engineering
Red Hat GmbH <https://www.redhat.com>
9704 A60C B4BE A8B8 0F30  9205 5D7E 4952 3F65 7898