MDS/openide
1
0
Fork 0
mirror of https://gitflic.ru/project/openide/openide.git synced 2026-10-01 19:02:13 +07:00
Code Issues Packages Projects Releases Wiki Activity

Find/Replace in editor: pixel hunting again

Browse Source
This commit is contained in:
Vassiliy.Kudryashov
2016-11-23 23:22:30 +03:00
parent b1f422867a
commit e1bf057603
1 changed files with 2 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
platform/lang-impl/src/com/intellij/find/SearchTextArea.java
+2 -3
View File
@@ -133,9 +133,8 @@ public class SearchTextArea extends NonOpaquePanel implements PropertyChangeList
protected void updateLayout() {
int height = UIUtil.getLineHeight(myTextArea);
Insets insets = myTextArea.getInsets();
height += insets.top + insets.bottom;
int extraGap = Math.max(0, (height - JBUI.scale(16)) / 2);
setBorder(new EmptyBorder(3, 6, 3, 4));
int extraGap = Math.max(JBUI.isHiDPI() ? 0 : 1, (height + insets.top + insets.bottom - JBUI.scale(16)) / 2);
setBorder(new EmptyBorder(3 + Math.max(0, JBUI.scale(16) - height) / 2, 6, 3, 4));//In case of small fonts we shouldn't align to top
setLayout(new MigLayout("flowx, ins 0, gapx " + JBUI.scale(4)));
removeAll();
add(myHistoryPopupButton, "ay top, gaptop " + extraGap +", gapleft" + (JBUI.isHiDPI() ? 4 : 0));