#1311 actionScript source font size

This commit is contained in:
2016-12-01 18:19:24 +01:00
parent 4d5d1cde53
commit 57ad8b667d
7 changed files with 25 additions and 15 deletions
+12 -8
View File
@@ -196,11 +196,11 @@ public class View {
FontPolicy pol = SubstanceLookAndFeel.getFontPolicy();
final FontSet fs = pol.getFontSet("Substance", null);
double fontSizeMultiplier = Configuration.guiFontSizeMultiplier.get();
//Restore default font for chinese characters
SubstanceLookAndFeel.setFontPolicy(new FontPolicy() {
private final FontSet fontSet = new FontSet() {
private FontUIResource controlFont;
private FontUIResource menuFont;
@@ -213,11 +213,15 @@ public class View {
private FontUIResource messageFont;
private int getFontSize(int defaultFontSize) {
return (int) (defaultFontSize * fontSizeMultiplier);
}
@Override
public FontUIResource getControlFont() {
if (controlFont == null) {
FontUIResource f = fs.getControlFont();
controlFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
controlFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return controlFont;
}
@@ -226,7 +230,7 @@ public class View {
public FontUIResource getMenuFont() {
if (menuFont == null) {
FontUIResource f = fs.getMenuFont();
menuFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
menuFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return menuFont;
}
@@ -235,7 +239,7 @@ public class View {
public FontUIResource getTitleFont() {
if (titleFont == null) {
FontUIResource f = fs.getTitleFont();
titleFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
titleFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return titleFont;
}
@@ -244,7 +248,7 @@ public class View {
public FontUIResource getWindowTitleFont() {
if (windowTitleFont == null) {
FontUIResource f = fs.getWindowTitleFont();
windowTitleFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
windowTitleFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return windowTitleFont;
}
@@ -253,7 +257,7 @@ public class View {
public FontUIResource getSmallFont() {
if (smallFont == null) {
FontUIResource f = fs.getSmallFont();
smallFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
smallFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return smallFont;
}
@@ -262,7 +266,7 @@ public class View {
public FontUIResource getMessageFont() {
if (messageFont == null) {
FontUIResource f = fs.getMessageFont();
messageFont = new FontUIResource(defaultFont.getName(), f.getStyle(), f.getSize());
messageFont = new FontUIResource(defaultFont.getName(), f.getStyle(), getFontSize(f.getSize()));
}
return messageFont;
}