diff options
author | Ian Trimble | 2013-04-23 00:04:47 +0000 |
---|---|---|
committer | Ian Trimble | 2013-04-23 00:04:47 +0000 |
commit | 5db5a4437a44464107a96de7684930213a481d9e (patch) | |
tree | 709e667f9acc1a27c826990c3a0df35e464f0020 | |
parent | d206b00a5780d7a28e82d7838e0640fefaba0d72 (diff) | |
download | webtools.jsf-5db5a4437a44464107a96de7684930213a481d9e.tar.gz webtools.jsf-5db5a4437a44464107a96de7684930213a481d9e.tar.xz webtools.jsf-5db5a4437a44464107a96de7684930213a481d9e.zip |
Bug 368375
Font size is very small in the Web Page Editor for some GTK/Linux
environments
-rw-r--r-- | jsf/plugins/org.eclipse.jst.pagedesigner/src/org/eclipse/jst/pagedesigner/css2/font/CSSFontManager.java | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/jsf/plugins/org.eclipse.jst.pagedesigner/src/org/eclipse/jst/pagedesigner/css2/font/CSSFontManager.java b/jsf/plugins/org.eclipse.jst.pagedesigner/src/org/eclipse/jst/pagedesigner/css2/font/CSSFontManager.java index 0297f9299..75bf202a9 100644 --- a/jsf/plugins/org.eclipse.jst.pagedesigner/src/org/eclipse/jst/pagedesigner/css2/font/CSSFontManager.java +++ b/jsf/plugins/org.eclipse.jst.pagedesigner/src/org/eclipse/jst/pagedesigner/css2/font/CSSFontManager.java @@ -11,6 +11,8 @@ *******************************************************************************/ package org.eclipse.jst.pagedesigner.css2.font; +import java.awt.Toolkit; + import org.eclipse.jst.pagedesigner.css2.ICSSStyle; import org.eclipse.jst.pagedesigner.css2.property.FontFamilyMeta; import org.eclipse.jst.pagedesigner.css2.property.FontSizeMeta; @@ -39,8 +41,28 @@ public class CSSFontManager implements ICSSFontManager { private static final int CACHESIZE = 100; // we cache 100 font. // the scale to convert the px to pt. - private final static double FONT_SCALE = ((double) Display.getCurrent() - .getDPI().x) / 72; + private final static double FONT_SCALE = getFontDPI() / 72; + + static double getFontDPI() { + //Bug 368375 - Font size is very small in the Web Page Editor for some GTK/Linux environments + double fontDPI = -1; + if ("gtk".equals(SWT.getPlatform())) { //$NON-NLS-1$ + Object value = Toolkit.getDefaultToolkit().getDesktopProperty("gnome.Xft/DPI"); //$NON-NLS-1$ + if (value instanceof Integer) { + fontDPI = ((Integer)value).intValue() / 1024; + if (fontDPI == -1) { + fontDPI = 96; + } + if (fontDPI < 50) { + fontDPI = 50; + } + } + } + if (fontDPI == -1) { + fontDPI = Display.getCurrent().getDPI().x; + } + return fontDPI; + } static String cssFontToLocalFont(String original) { if ("serif".equalsIgnoreCase(original)) { //$NON-NLS-1$ |