Console/error/whatever tabs at the bottom of the editor window.
| 47 | * Console/error/whatever tabs at the bottom of the editor window. |
| 48 | */ |
| 49 | public class ManagerTabs extends Box { |
| 50 | // height of this tab bar |
| 51 | static final int HIGH = Toolkit.zoom(34); |
| 52 | |
| 53 | // amount of space around the entire window |
| 54 | static final int BORDER = Toolkit.zoom(8); |
| 55 | |
| 56 | static final int CURVE_RADIUS = Toolkit.zoom(6); |
| 57 | |
| 58 | static final int TAB_TOP = Toolkit.zoom(0); |
| 59 | static final int TAB_BOTTOM = HIGH - Toolkit.zoom(2); |
| 60 | // amount of extra space between individual tabs |
| 61 | static final int TAB_BETWEEN = Toolkit.zoom(2); |
| 62 | // amount of margin on the left/right for the text on the tab |
| 63 | static final int MARGIN = Toolkit.zoom(14); |
| 64 | |
| 65 | static final int ICON_WIDTH = Toolkit.zoom(16); |
| 66 | static final int ICON_HEIGHT = Toolkit.zoom(16); |
| 67 | static final int ICON_TOP = Toolkit.zoom(7); |
| 68 | static final int ICON_MARGIN = Toolkit.zoom(7); |
| 69 | |
| 70 | static final int UNSELECTED = 0; |
| 71 | static final int SELECTED = 1; |
| 72 | |
| 73 | Color[] textColor = new Color[2]; |
| 74 | Color[] tabColor = new Color[2]; |
| 75 | |
| 76 | List<Tab> tabList = new ArrayList<>(); |
| 77 | |
| 78 | Mode mode; |
| 79 | |
| 80 | Font font; |
| 81 | int fontAscent; |
| 82 | |
| 83 | Image offscreen; |
| 84 | int sizeW, sizeH; |
| 85 | int imageW, imageH; |
| 86 | |
| 87 | Image gradient; |
| 88 | |
| 89 | JPanel cardPanel; |
| 90 | CardLayout cardLayout; |
| 91 | Controller controller; |
| 92 | |
| 93 | Component currentPanel; |
| 94 | |
| 95 | |
| 96 | public ManagerTabs(Base base) { |
| 97 | super(BoxLayout.Y_AXIS); |
| 98 | |
| 99 | // A mode shouldn't actually override these, they're coming from theme.txt. |
| 100 | // But use the default (Java) mode settings just in case. |
| 101 | mode = base.getDefaultMode(); |
| 102 | |
| 103 | textColor[SELECTED] = mode.getColor("manager.tab.text.selected.color"); |
| 104 | textColor[UNSELECTED] = mode.getColor("manager.tab.text.unselected.color"); |
| 105 | font = mode.getFont("manager.tab.text.font"); |
| 106 |