From 3ed29a58335377e6d39998adf8c874930a6c4e69 Mon Sep 17 00:00:00 2001 From: Ben Fry Date: Sat, 22 Apr 2017 12:02:50 -0400 Subject: [PATCH] also scale the gap around tooltips (#4914) --- app/src/processing/app/ui/Editor.java | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index 9bb480930..262ff8903 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -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 = "
" + message + "
"; comp.setToolTipText(content);