From c9140cf6868dd3527a888762931f89069dd7bc66 Mon Sep 17 00:00:00 2001 From: soarcreator Date: Tue, 18 Sep 2018 17:23:59 -0700 Subject: [PATCH] Allow tabs to adjust their size when there are too many tabs I fixed the problem when there are too many tabs on the Editor header. When the remaining space is not enough, all tabs become as small as it is necessary to be to squash into the space. --- app/src/processing/app/EditorHeader.java | 37 ++++++++++++++++++++---- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/app/src/processing/app/EditorHeader.java b/app/src/processing/app/EditorHeader.java index 25c09a8dfaa..2e36a4c3dfe 100644 --- a/app/src/processing/app/EditorHeader.java +++ b/app/src/processing/app/EditorHeader.java @@ -32,6 +32,7 @@ import java.awt.*; import java.awt.event.*; import java.io.IOException; +import java.util.ArrayList; import java.util.List; import javax.swing.*; @@ -241,19 +242,45 @@ public void paintComponent(Graphics screen) { tabRight = new int[codeCount]; } - int x = scale(6); // offset from left edge of the component - int i = 0; + List texts = new ArrayList(); + int totalWidth = 0; for (EditorTab tab : tabs) { SketchFile file = tab.getSketchFile(); String filename = file.getPrettyName(); // if modified, add the li'l glyph next to the name - String text = " " + filename + (file.isModified() ? " \u00A7" : " "); + String text = filename; + if (file.isModified()) + text += " \u00A7"; + texts.add(text); + + int textWidth = (int) + font.getStringBounds(text, g.getFontRenderContext()).getWidth(); + + int pieceCount = textWidth / PIECE_WIDTH; + int pieceWidth = pieceCount * PIECE_WIDTH; + totalWidth += PIECE_WIDTH * (pieceCount + 2) - 1; // left + middle + right - overlap(=1) + } + + int marginPieceCount = 0; + int marginForEveryPiece = PIECE_WIDTH * tabs.size(); + for (int i = 1; i <= 6; ++i) { + if (sizeW - totalWidth > marginForEveryPiece * i) { + marginPieceCount = i; + continue; + } + break; + } + + int x = scale(6); // offset from left edge of the component + int i = 0; + for (EditorTab tab : tabs) { + String text = texts.get(i); int textWidth = (int) font.getStringBounds(text, g.getFontRenderContext()).getWidth(); - int pieceCount = 2 + (textWidth / PIECE_WIDTH); + int pieceCount = marginPieceCount + (textWidth / PIECE_WIDTH); int pieceWidth = pieceCount * PIECE_WIDTH; int state = (i == editor.getCurrentTabIndex()) ? SELECTED : UNSELECTED; @@ -276,7 +303,7 @@ public void paintComponent(Graphics screen) { g.drawImage(pieces[state][RIGHT], x, 0, null); x += PIECE_WIDTH - 1; // overlap by 1 pixel - i++; + ++i; } menuLeft = sizeW - (16 + menuButtons[0].getWidth(this));