From 8ba1d31b98f612f55cbf65ea757692ac7f264895 Mon Sep 17 00:00:00 2001
From: Vadim Lopatin <coolreader.org@gmail.com>
Date: Thu, 7 Sep 2017 11:37:30 +0300
Subject: [PATCH] setting for editor font size - close #249

---
 src/dlangide/ui/dsourceedit.d        | 7 +++++++
 src/dlangide/ui/settings.d           | 2 ++
 src/dlangide/workspace/idesettings.d | 7 ++++---
 views/VERSION                        | 2 +-
 4 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/dlangide/ui/dsourceedit.d b/src/dlangide/ui/dsourceedit.d
index 86530dd..046dd16 100644
--- a/src/dlangide/ui/dsourceedit.d
+++ b/src/dlangide/ui/dsourceedit.d
@@ -95,6 +95,7 @@ class DSourceEdit : SourceEdit, EditableContentMarksChangeListener {
     @property IDESettings settings() {
         return _settings;
     }
+    protected int _previousFontSizeSetting;
     void applySettings() {
         if (!_settings)
             return;
@@ -111,6 +112,12 @@ class DSourceEdit : SourceEdit, EditableContentMarksChangeListener {
             face ~= ",";
         face ~= DEFAULT_SOURCE_EDIT_FONT_FACES;
         fontFace = face;
+        int newFontSizeSetting = _settings.editorFontSize;
+        bool needChangeFontSize = _previousFontSizeSetting == 0 || (_previousFontSizeSetting != newFontSizeSetting && _previousFontSizeSetting.pointsToPixels == fontSize);
+        if (needChangeFontSize) {
+            fontSize = newFontSizeSetting.pointsToPixels;
+            _previousFontSizeSetting = newFontSizeSetting;
+        }
     }
 
     protected EditorTool _editorTool;
diff --git a/src/dlangide/ui/settings.d b/src/dlangide/ui/settings.d
index 6abacc5..384c094 100644
--- a/src/dlangide/ui/settings.d
+++ b/src/dlangide/ui/settings.d
@@ -122,6 +122,8 @@ SettingsPage createSettingsPages() {
 
     // editor font faces
     texted.addStringComboBox("editors/textEditor/fontFace", UIString.fromId("OPTION_FONT_FACE"c), createFaceList(true));
+    texted.addIntComboBox("editors/textEditor/fontSize", UIString.fromId("OPTION_FONT_SIZE"c),
+                      createIntValueList([6,7,8,9,10,11,12,14,16,18,20,22,24,26,28,30,32]));
 
     texted.addNumberEdit("editors/textEditor/tabSize", UIString.fromId("OPTION_TAB"c), 1, 16, 4);
     texted.addCheckbox("editors/textEditor/useSpacesForTabs", UIString.fromId("OPTION_USE_SPACES"c));
diff --git a/src/dlangide/workspace/idesettings.d b/src/dlangide/workspace/idesettings.d
index f70e6a8..2e4f4f1 100644
--- a/src/dlangide/workspace/idesettings.d
+++ b/src/dlangide/workspace/idesettings.d
@@ -24,6 +24,7 @@ class IDESettings : SettingsFile {
         ed.setBooleanDef("showWhiteSpaceMarks", true);
         ed.setBooleanDef("showTabPositionMarks", true);
         ed.setStringDef("fontFace", "Default");
+        ed.setIntegerDef("fontSize", 11);
         Setting ui = uiSettings();
         ui.setStringDef("theme", "ide_theme_default");
         ui.setStringDef("language", "en");
@@ -170,10 +171,10 @@ class IDESettings : SettingsFile {
     @property bool showTabPositionMarks() { return editorSettings.getBoolean("showTabPositionMarks", true); }
     /// set tab position marks enabled flag
     @property IDESettings showTabPositionMarks(bool enabled) { editorSettings.setBoolean("showTabPositionMarks", enabled); return this; }
-    /// string value of font face
+    /// string value of font face in text editors
     @property string editorFontFace() { return editorSettings.getString("fontFace", "Default"); }
-
-    
+    /// int value of font size in text editors
+    @property int editorFontSize() { return cast(int)editorSettings.getInteger("fontSize", 11); }
 
     /// true if smart indents are enabled
     @property bool smartIndentsAfterPaste() { return editorSettings.getBoolean("smartIndentsAfterPaste", true); }
diff --git a/views/VERSION b/views/VERSION
index c5441ad..fa3421c 100644
--- a/views/VERSION
+++ b/views/VERSION
@@ -1 +1 @@
-v0.7.67
\ No newline at end of file
+v0.7.68
\ No newline at end of file