From a318577f97054bb31a2c660ac41938ef76e95e08 Mon Sep 17 00:00:00 2001
From: Vadim Lopatin <coolreader.org@gmail.com>
Date: Fri, 25 Aug 2017 17:01:25 +0300
Subject: [PATCH] apply ui font changes

---
 src/dlangide/ui/frame.d              | 16 ++++++++++++++++
 src/dlangide/workspace/idesettings.d | 10 ++++++++++
 2 files changed, 26 insertions(+)

diff --git a/src/dlangide/ui/frame.d b/src/dlangide/ui/frame.d
index aca5865..f7e9048 100644
--- a/src/dlangide/ui/frame.d
+++ b/src/dlangide/ui/frame.d
@@ -1354,6 +1354,22 @@ class IDEFrame : AppFrame, ProgramExecutionStatusListener, BreakpointListChangeL
         FontManager.minAnitialiasedFontSize = settings.minAntialiasedFontSize;
         Platform.instance.uiLanguage = settings.uiLanguage;
         Platform.instance.uiTheme = settings.uiTheme;
+        bool needUpdateTheme = false;
+        string oldFontFace = currentTheme.fontFace;
+        string newFontFace = settings.uiFontFace;
+        if (newFontFace == "Default")
+            newFontFace = "Helvetica Neue,Verdana,Arial,DejaVu Sans,Liberation Sans,Helvetica,Roboto,Droid Sans";
+        int oldFontSize = currentTheme.fontSize;
+        if (oldFontFace != newFontFace) {
+            currentTheme.fontFace = newFontFace;
+            needUpdateTheme = true;
+        }
+        if (oldFontSize != settings.uiFontSize) {
+            currentTheme.fontSize = settings.uiFontSize;
+            needUpdateTheme = true;
+        }
+        if (needUpdateTheme)
+            Platform.instance.onThemeChanged();
         requestLayout();
     }
 
diff --git a/src/dlangide/workspace/idesettings.d b/src/dlangide/workspace/idesettings.d
index 5e0e495..f70e6a8 100644
--- a/src/dlangide/workspace/idesettings.d
+++ b/src/dlangide/workspace/idesettings.d
@@ -126,6 +126,16 @@ class IDESettings : SettingsFile {
         return this;
     }
 
+    /// UI font face
+    @property string uiFontFace() {
+        return uiSettings.getString("uiFontFace", "Default");
+    }
+
+    /// UI font size
+    @property int uiFontSize() {
+        return pointsToPixels(cast(int)uiSettings.getInteger("uiFontSize", 10));
+    }
+
     /// text editor setting, true if need to insert spaces instead of tabs
     @property bool useSpacesForTabs() {
         return editorSettings.getBoolean("useSpacesForTabs", true);