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

Marcus Hirt marcus.hirt at oracle.com
Thu Dec 6 18:34:30 UTC 2018


Hi Elliott,

Just one nit - don't forget to put //$NON-NLS-1$ tags on string constants that 
should not be localized, e.g.:

private static final String FIXED_TEXT_FONT = "org.openjdk.jmc.fixedtextfont"; //$NON-NLS-1$

Looks fine - don't need another review after fixing this. 

Thank you for your contribution!

Kind regards,
Marcus

On 2018-12-04, 01:24, "jmc-dev on behalf of Elliott Baron" <jmc-dev-bounces at openjdk.java.net on behalf of ebaron at redhat.com> wrote:

    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
    
    




More information about the jmc-dev mailing list