import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
+import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
private static final int MAX_LABEL_LENGTH = 256;
+ private static final int PPI = 72; // points per inch
+ private static final int DPI = Display.getDefault().getDPI().y;
+
/** Resource manager */
private LocalResourceManager fResourceManager = new LocalResourceManager(JFaceResources.getResources());
private boolean fMouseOverSplitLine = false;
private int fGlobalItemHeight = CUSTOM_ITEM_HEIGHT;
private int fHeightAdjustment = 0;
- private int fInitialFontHeight;
- private Font fFont;
+ private Map<Integer, Font> fFonts = new HashMap<>();
private boolean fBlendSubPixelEvents = false;
private int fMinimumItemWidth = 0;
private int fTopIndex = 0;
public void dispose() {
super.dispose();
fResourceManager.dispose();
- if (fFont != null) {
- fFont.dispose();
+ for (Font font : fFonts.values()) {
+ font.dispose();
}
}
*
* @param zoomIn
* true to zoom in, false to zoom out
- * @param adjustItems
- * true to adjust item heights, false to adjust font only
* @since 2.0
*/
- public void verticalZoom(boolean zoomIn, boolean adjustItems) {
+ public void verticalZoom(boolean zoomIn) {
if (zoomIn) {
fHeightAdjustment++;
} else {
fHeightAdjustment--;
}
- FontData fontData = getFont().getFontData()[0];
- if (fInitialFontHeight == 0) {
- fInitialFontHeight = fontData.getHeight();
- }
- int height = Math.max(1, fInitialFontHeight + fHeightAdjustment);
- fontData.setHeight(height);
- if (fFont != null) {
- fFont.dispose();
- }
- fFont = new Font(getDisplay(), fontData);
- setFont(fFont);
- if (adjustItems) {
- fItemData.refreshData();
- }
+ fItemData.refreshData();
redraw();
}
/**
* Reset the vertical zoom to default.
*
- * @param adjustItems
- * true to reset item heights, false to reset font only
* @since 2.0
*/
- public void resetVerticalZoom(boolean adjustItems) {
+ public void resetVerticalZoom() {
fHeightAdjustment = 0;
- if (fFont != null) {
- fFont.dispose();
- fFont = null;
- }
- setFont(null);
- if (adjustItems) {
- fItemData.refreshData();
- }
+ fItemData.refreshData();
redraw();
}
if (item.fEntry.hasTimeEvents()) {
gc.setClipping(new Rectangle(nameSpace, 0, bounds.width - nameSpace, bounds.height));
fillSpace(rect, gc, selected);
- /*
- * State rectangle is smaller than item bounds. Use a margin height
- * of 3 pixels, keep at least 3 pixels for the state, but not more
- * than the item height. Favor the top margin for the remainder.
- */
- int height = Math.min(rect.height, Math.max(3, rect.height - 6));
- int margin = (rect.height - height + 1) / 2;
- Rectangle stateRect = new Rectangle(rect.x, rect.y + margin, rect.width, height);
+
+ int margins = getMarginForHeight(rect.height);
+ int height = rect.height - margins;
+ int topMargin = (margins + 1) / 2;
+ Rectangle stateRect = new Rectangle(rect.x, rect.y + topMargin, rect.width, height);
+
+ /* Set the font for this item */
+ setFontForHeight(height, gc);
long maxDuration = (timeProvider.getTimeSpace() == 0) ? Long.MAX_VALUE : 1 * (time1 - time0) / timeProvider.getTimeSpace();
Iterator<ITimeEvent> iterator = entry.getTimeEventsIterator(time0, time1, maxDuration);
return;
}
+ int height = bounds.height - getMarginForHeight(bounds.height);
+ setFontForHeight(height, gc);
+
int leftMargin = MARGIN + item.fLevel * EXPAND_SIZE;
if (item.fHasChildren) {
gc.setForeground(getColorScheme().getFgColorGroup(false, false));
gc.drawLine(rect.x, midy, rect.x + rect.width, midy);
}
+ private static int getMarginForHeight(int height) {
+ /*
+ * State rectangle is smaller than the item bounds when height is > 4.
+ * Don't use any margin if the height is below or equal that threshold.
+ * Use a maximum of 6 pixels for both margins, otherwise try to use 13
+ * pixels for the state height, but with a minimum margin of 1.
+ */
+ final int MARGIN_THRESHOLD = 4;
+ final int PREFERRED_HEIGHT = 13;
+ final int MIN_MARGIN = 1;
+ final int MAX_MARGIN = 6;
+ return height <= MARGIN_THRESHOLD ? 0 :
+ Math.max(Math.min(height - PREFERRED_HEIGHT, MAX_MARGIN), MIN_MARGIN);
+ }
+
+ private void setFontForHeight(int pixels, GC gc) {
+ /* convert font height from pixels to points */
+ int height = Math.max(pixels * PPI / DPI, 1);
+ Font font = fFonts.get(height);
+ if (font == null) {
+ FontData fontData = gc.getFont().getFontData()[0];
+ fontData.setHeight(height);
+ font = new Font(gc.getDevice(), fontData);
+ fFonts.put(height, font);
+ }
+ gc.setFont(font);
+ }
+
@Override
public void keyTraversed(TraverseEvent e) {
if ((e.detail == SWT.TRAVERSE_TAB_NEXT) || (e.detail == SWT.TRAVERSE_TAB_PREVIOUS)) {
}
idx = -1;
} else if ((e.character == '+' || e.character == '=') && ((e.stateMask & SWT.CTRL) != 0)) {
- verticalZoom(true, true);
+ verticalZoom(true);
} else if (e.character == '-' && ((e.stateMask & SWT.CTRL) != 0)) {
- verticalZoom(false, true);
+ verticalZoom(false);
} else if (e.character == '0' && ((e.stateMask & SWT.CTRL) != 0)) {
- resetVerticalZoom(true);
+ resetVerticalZoom();
}
if (idx >= 0) {
selectItem(idx, false);
if (fDragState != DRAG_NONE) {
return;
}
- boolean zoomScroll = false;
+ boolean horizontalZoom = false;
boolean horizontalScroll = false;
+ boolean verticalZoom = false;
Point p = getParent().toControl(getDisplay().getCursorLocation());
Point parentSize = getParent().getSize();
if (p.x >= 0 && p.x < parentSize.x && p.y >= 0 && p.y < parentSize.y) {
// over the parent control
if (e.x > getSize().x) {
// over the vertical scroll bar
- zoomScroll = false;
+ if ((e.stateMask & SWT.MODIFIER_MASK) == (SWT.SHIFT | SWT.CTRL)) {
+ verticalZoom = true;
+ }
} else if (e.y < 0) {
// over the time scale
- zoomScroll = true;
+ horizontalZoom = true;
} else if (e.y >= getSize().y) {
// over the horizontal scroll bar
if ((e.stateMask & SWT.MODIFIER_MASK) == SWT.CTRL) {
- zoomScroll = true;
+ horizontalZoom = true;
} else {
horizontalScroll = true;
}
} else {
- if (e.x < fTimeProvider.getNameSpace()) {
+ if ((e.stateMask & SWT.MODIFIER_MASK) == (SWT.SHIFT | SWT.CTRL)) {
+ verticalZoom = true;
+ } else if (e.x < fTimeProvider.getNameSpace()) {
// over the name space
- zoomScroll = false;
+ horizontalZoom = false;
} else {
// over the state area
if ((e.stateMask & SWT.MODIFIER_MASK) == SWT.CTRL) {
// over the state area, CTRL pressed
- zoomScroll = true;
+ horizontalZoom = true;
} else {
// over the state area, CTRL not pressed
- zoomScroll = false;
+ horizontalZoom = false;
}
}
}
}
- if (zoomScroll && fTimeProvider.getTime0() != fTimeProvider.getTime1()) {
+ if (verticalZoom) {
+ if (e.count > 0) {
+ verticalZoom(true);
+ } else if (e.count < 0) {
+ verticalZoom(false);
+ }
+ } else if (horizontalZoom && fTimeProvider.getTime0() != fTimeProvider.getTime1()) {
if (e.count > 0) {
zoom(true);
} else if (e.count < 0) {