From 0ce1fb67c6111ed68a7ea4f0c891e8820c2acd2b Mon Sep 17 00:00:00 2001 From: AlexisDrogoul Date: Sat, 17 Jul 2021 11:36:59 +0700 Subject: [PATCH] More experiments with default button heights --- .../src/ummisco/gama/ui/controls/FlatButton.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/ummisco.gama.ui.shared/src/ummisco/gama/ui/controls/FlatButton.java b/ummisco.gama.ui.shared/src/ummisco/gama/ui/controls/FlatButton.java index 6085f16153..cb4ecaeaf4 100644 --- a/ummisco.gama.ui.shared/src/ummisco/gama/ui/controls/FlatButton.java +++ b/ummisco.gama.ui.shared/src/ummisco/gama/ui/controls/FlatButton.java @@ -72,9 +72,9 @@ public static FlatButton menu(final Composite comp, final GamaUIColor color, fin private String text; private RGB colorCode; private static final int innerMarginWidth = 5; - private static int DEFAULT_HEIGHT = - WorkbenchHelper.getDisplay().getSystemFont().getFontData()[0].getHeight() + innerMarginWidth; - private int height = DEFAULT_HEIGHT; + // private static int DEFAULT_HEIGHT = + // WorkbenchHelper.getDisplay().getSystemFont().getFontData()[0].getHeight() + innerMarginWidth; + private int height = -1; // DEFAULT_HEIGHT; private static final int imagePadding = 5; private boolean enabled = true; private boolean hovered = false; @@ -278,7 +278,7 @@ public int computeMinHeight() { } if (text != null) { final GC gc = new GC(this); - // gc.setFont(getFont()); + gc.setFont(getFont()); final Point extent = gc.textExtent(text + "..."); gc.dispose(); height = Math.max(height, extent.y + innerMarginWidth); @@ -403,6 +403,7 @@ public FlatButton setColor(final GamaUIColor c) { } public int getHeight() { + if (height == -1) { height = computeMinHeight(); } return height; }