rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-26 20:54:22 +01:00
Code Issues Releases Activity

Shift tabs if selected one if being painted offscreen

Browse Source 
Implemented using a dry run to get the metrics and the needed shift
Fixes #1193 and #6109
This commit is contained in:
Martino Facchin 2017-09-11 17:39:34 +02:00
parent 2bcbaf7a68
commit 578d34e203
1 changed files with 47 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
app/src/processing/app/EditorHeader.java
View File

@ -243,6 +243,52 @@ public class EditorHeader extends JComponent {
int x = scale(6); // offset from left edge of the component int x = scale(6); // offset from left edge of the component
int i = 0; int i = 0;
int x_selected = 0;
// dry run, get the correct offset
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" : " ");
int textWidth = (int)
font.getStringBounds(text, g.getFontRenderContext()).getWidth();
int pieceCount = 2 + (textWidth / PIECE_WIDTH);
int pieceWidth = pieceCount * PIECE_WIDTH;
int state = (i == editor.getCurrentTabIndex()) ? SELECTED : UNSELECTED;
x += PIECE_WIDTH;
int contentLeft = x;
tabLeft[i] = x;
for (int j = 0; j < pieceCount; j++) {
x += PIECE_WIDTH;
}
tabRight[i] = x;
int textLeft = contentLeft + (pieceWidth - textWidth) / 2;
int baseline = (sizeH + fontAscent) / 2;
//g.drawString(sketch.code[i].name, textLeft, baseline);
x += PIECE_WIDTH - 1; // overlap by 1 pixel
if (state == SELECTED) {
x_selected = x;
}
i++;
}
if (x_selected > imageW) {
x = -(x_selected - imageW);
} else {
x = scale(6); // offset from left edge of the component
}
i = 0;
for (EditorTab tab : tabs) { for (EditorTab tab : tabs) {
SketchFile file = tab.getSketchFile(); SketchFile file = tab.getSketchFile();
String filename = file.getPrettyName(); String filename = file.getPrettyName();
@ -276,6 +322,7 @@ public class EditorHeader extends JComponent {
g.drawImage(pieces[state][RIGHT], x, 0, null); g.drawImage(pieces[state][RIGHT], x, 0, null);
x += PIECE_WIDTH - 1; // overlap by 1 pixel x += PIECE_WIDTH - 1; // overlap by 1 pixel
i++; i++;
} }