mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
use small font for editor when tabs font is small
This commit is contained in:
@@ -29,6 +29,7 @@ import com.intellij.ui.tabs.TabsListener;
|
||||
import com.intellij.ui.tabs.impl.JBEditorTabs;
|
||||
import com.intellij.ui.tabs.impl.JBTabsImpl;
|
||||
import com.intellij.ui.tabs.impl.TabLabel;
|
||||
import com.intellij.util.ui.UIUtil;
|
||||
import com.jediterm.terminal.ui.*;
|
||||
import com.jediterm.terminal.ui.settings.SettingsProvider;
|
||||
import org.jetbrains.annotations.NotNull;
|
||||
@@ -346,6 +347,9 @@ public class JBTabbedTerminalWidget extends TabbedTerminalWidget implements Disp
|
||||
return new Dimension(minimalWidth + 10, size.height);
|
||||
}
|
||||
};
|
||||
if (myTabs.useSmallLabels()) {
|
||||
textField.setFont(com.intellij.util.ui.UIUtil.getFont(UIUtil.FontSize.SMALL, textField.getFont()));
|
||||
}
|
||||
textField.setOpaque(true);
|
||||
return textField;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user