JIDE: JideTabbedPane: scale tab gripper

This commit is contained in:
Karl Tauber
2021-03-27 17:48:58 +01:00
parent d7b0754327
commit 69f52c8abd
4 changed files with 43 additions and 0 deletions

View File

@@ -107,4 +107,22 @@ public class FlatJidePainter
} else
super.paintBackground( c, g, rect, borderColor, background, orientation );
}
@Override
public void paintGripper( JComponent c, Graphics g, Rectangle rect, int orientation, int state ) {
float userScaleFactor = UIScale.getUserScaleFactor();
if( userScaleFactor > 1 ) {
// scale gripper
Graphics2D g2 = (Graphics2D) g.create();
try {
g2.translate( rect.x, rect.y );
g2.scale( userScaleFactor, userScaleFactor );
Rectangle rect2 = new Rectangle( 0, 0, UIScale.unscale( rect.width ), UIScale.unscale( rect.height ) );
super.paintGripper( c, g2, rect2, orientation, state );
} finally {
g2.dispose();
}
} else
super.paintGripper( c, g, rect, orientation, state );
}
}

View File

@@ -151,6 +151,7 @@ public class FlatJideTabbedPaneUI
case JideTabbedPane.PROPERTY_TAB_AREA_INSETS:
case JideTabbedPane.PROPERTY_TAB_INSETS:
case JideTabbedPane.GRIPPER_PROPERTY:
case TABBED_PANE_SHOW_TAB_SEPARATORS:
case TABBED_PANE_HAS_FULL_BORDER:
_tabPane.revalidate();