also scale the gap around tooltips (#4914)

This commit is contained in:
Ben Fry
2017-04-22 12:02:50 -04:00
parent 1e1b9e3f98
commit 3ed29a5833
+5 -3
View File
@@ -3156,18 +3156,20 @@ public abstract class Editor extends JFrame implements RunnerListener {
public void statusToolTip(JComponent comp, String message, boolean error) {
if (font == null) {
font = Toolkit.getSansFont(9, Font.PLAIN);
font = Toolkit.getSansFont(Toolkit.zoom(9), Font.PLAIN);
textColor = mode.getColor("errors.selection.fgcolor");
bgColorWarning = mode.getColor("errors.selection.warning.bgcolor");
bgColorError = mode.getColor("errors.selection.error.bgcolor");
}
Color bgColor = error ? bgColorError : bgColorWarning;
int m = Toolkit.zoom(3);
String css =
"margin: -3 -3 -3 -3; padding: 3 3 3 3; " +
String.format("margin: %d %d %d %d; ", -m, -m, -m, -m) +
String.format("padding: %d %d %d %d; ", m, m, m, m) +
"background: #" + PApplet.hex(bgColor.getRGB(), 8).substring(2) + ";" +
"font-family: " + font.getFontName() + ", sans-serif;" +
"font-size: " + Toolkit.zoom(font.getSize()) + "px;";
"font-size: " + font.getSize() + "px;";
String content =
"<html> <div style='" + css + "'>" + message + "</div> </html>";
comp.setToolTipText(content);