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

[Elliott Baron]

Hi,

This patch fixes an issue where font sizes vary between columns of 
certain trees and tables, when the user changes the editor font size. 
This happens for columns that use the JFace text font, which is also 
used for text editors in Eclipse. The text font is used as a visual hint 
for columns that may contain editable values. Other columns use the 
JFace default font, which derives from the native system default.

This simple fix creates a separate font, derived from the JFace text 
font, that sets its height to that of the default font. This ensures 
tree/table columns have consistent font sizes, while also retaining the 
text font face as an indicator for modifiable fields. The font is added 
to the shared JFace FontRegistry, and is disposed of along with the Display.

I have included a new UI test case to verify that our modified font is 
used for the LabelProvider that was previously using the JFace text font.

While I made progress towards some of the other goals mentioned in the 
bug, such as allowing all text in JMC to have its size adjusted using 
keyboard shortcuts, we decided to defer such a far-reaching change to a 
later date [1]. Perhaps we could create another bug for such a feature.

How does the attached patch look?

Thanks,
Elliott

[1] http://mail.openjdk.java.net/pipermail/jmc-dev/2018-November/000456.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: jmc-6180.patch
Type: text/x-patch
Size: 10355 bytes
Desc: not available
URL: <http://mail.openjdk.java.net/pipermail/jmc-dev/attachments/20181203/42526aa0/jmc-6180-0001.patch>