Set font size in code editor from the settings page (#140)

www/code/inner.js

@@ -239,24 +239,28 @@ define([
     };
 
     var mkIndentSettings = function (editor, metadataMgr) {
-        var setIndentation = function (units, useTabs) {
+        var setIndentation = function (units, useTabs, fontSize) {
             if (typeof(units) !== 'number') { return; }
             editor.setOption('indentUnit', units);
             editor.setOption('tabSize', units);
             editor.setOption('indentWithTabs', useTabs);
+            $('.CodeMirror').css('font-size', fontSize+'px');
         };
 
         var indentKey = 'indentUnit';
         var useTabsKey = 'indentWithTabs';
+        var fontKey = 'fontSize';
         var updateIndentSettings = function () {
             if (!metadataMgr) { return; }
             var data = metadataMgr.getPrivateData().settings;
             data = data.codemirror || {};
             var indentUnit = data[indentKey];
             var useTabs = data[useTabsKey];
+            var fontSize = data[fontKey];
             setIndentation(
                 typeof(indentUnit) === 'number'? indentUnit : 2,
-                typeof(useTabs) === 'boolean'? useTabs: false);
+                typeof(useTabs) === 'boolean'? useTabs : false,
+                typeof(fontSize) === 'number' ? fontSize : 12);
         };
         metadataMgr.onChangeLazy(updateIndentSettings);
         updateIndentSettings();

www/common/translations/messages.js

@@ -643,6 +643,7 @@ define(function () {
 
     out.settings_codeIndentation = 'Code editor indentation (spaces)';
     out.settings_codeUseTabs = "Indent using tabs (instead of spaces)";
+    out.settings_codeFontSize = "Font size in the code editor";
 
     out.settings_padWidth = "Editor's maximum width";
     out.settings_padWidthHint = "Rich text pads use by default the maximum available width on your screen and it can be difficult to read. You can reduce the editor's width here.";

www/settings/inner.js

@@ -73,7 +73,8 @@ define([
         ],
         'code': [
             'cp-settings-code-indent-unit',
-            'cp-settings-code-indent-type'
+            'cp-settings-code-indent-type',
+            'cp-settings-code-font-size',
         ],
         'subscription': {
             onClick: function () {
@@ -1207,6 +1208,39 @@ define([
         return $div;
     };
 
+    create['code-font-size'] = function () {
+        var key = 'fontSize';
+
+        var $div = $('<div>', {
+            'class': 'cp-settings-code-font-size cp-sidebarlayout-element'
+        });
+        $('<label>').text(Messages.settings_codeFontSize).appendTo($div);
+
+        var $inputBlock = $('<div>', {
+            'class': 'cp-sidebarlayout-input-block',
+        }).appendTo($div);
+
+        var $input = $('<input>', {
+            'min': 8,
+            'max': 30,
+            type: 'number',
+        }).on('change', function () {
+            var val = parseInt($input.val());
+            if (typeof(val) !== 'number') { return; }
+            common.setAttribute(['codemirror', key], val);
+        }).appendTo($inputBlock);
+
+        common.getAttribute(['codemirror', key], function (e, val) {
+            if (e) { return void console.error(e); }
+            if (typeof(val) !== 'number') {
+                $input.val(12);
+            } else {
+                $input.val(val);
+            }
+        });
+        return $div;
+    };
+
     // Settings app
 
     var createUsageButton = function () {