mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
get rid of double border between editor header component and editor in case of tab placement != top
This commit is contained in:
+1
-2
@@ -28,10 +28,9 @@ import java.awt.*;
|
||||
* @author gregsh
|
||||
*/
|
||||
public class EditorHeaderComponent extends JPanel {
|
||||
|
||||
public EditorHeaderComponent() {
|
||||
super(new BorderLayout(0, 0));
|
||||
setBorder(new CustomLineBorder(JBColor.border(), 0, UIUtil.isUnderGTKLookAndFeel()? 0 : 1, 1, 0));
|
||||
setBorder(new CustomLineBorder(JBColor.border(), 0, 0, 1, 0));
|
||||
}
|
||||
|
||||
@Override
|
||||
|
||||
@@ -6832,7 +6832,10 @@ public final class EditorImpl extends UserDataHolderBase implements EditorEx, Hi
|
||||
Container splitters = SwingUtilities.getAncestorOfClass(EditorsSplitters.class, c);
|
||||
boolean thereIsSomethingAbove = !SystemInfo.isMac || UISettings.getInstance().SHOW_MAIN_TOOLBAR || UISettings.getInstance().SHOW_NAVIGATION_BAR ||
|
||||
toolWindowIsNotEmpty();
|
||||
return splitters == null ? super.getBorderInsets(c) : new Insets(thereIsSomethingAbove ? 1 : 0, 0, 0, 0);
|
||||
//noinspection ConstantConditions
|
||||
Component header = myHeaderPanel == null ? null : ArrayUtil.getFirstElement(myHeaderPanel.getComponents());
|
||||
boolean paintTop = thereIsSomethingAbove && header == null && UISettings.getInstance().EDITOR_TAB_PLACEMENT != SwingConstants.TOP;
|
||||
return splitters == null ? super.getBorderInsets(c) : new Insets(paintTop ? 1 : 0, 0, 0, 0);
|
||||
}
|
||||
|
||||
public boolean toolWindowIsNotEmpty() {
|
||||
|
||||
Reference in New Issue
Block a user