From 150b3c100a79a973f99cb0c061acce46b4757775 Mon Sep 17 00:00:00 2001
From: Dennis Ushakov <dennis.ushakov@gmail.com>
Date: Tue, 18 Mar 2014 11:19:02 +0400
Subject: [PATCH] use small font for editor when tabs font is small

---
 .../jetbrains/plugins/terminal/JBTabbedTerminalWidget.java    | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/plugins/terminal/src/org/jetbrains/plugins/terminal/JBTabbedTerminalWidget.java b/plugins/terminal/src/org/jetbrains/plugins/terminal/JBTabbedTerminalWidget.java
index 9b595a9209b5..d39d2ec09b71 100644
--- a/plugins/terminal/src/org/jetbrains/plugins/terminal/JBTabbedTerminalWidget.java
+++ b/plugins/terminal/src/org/jetbrains/plugins/terminal/JBTabbedTerminalWidget.java
@@ -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;
           }