diff --git a/www/code/inner.js b/www/code/inner.js index 88515e638..2376c80bb 100644 --- a/www/code/inner.js +++ b/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(indentUnit) === 'number'? indentUnit : 2, + typeof(useTabs) === 'boolean'? useTabs : false, + typeof(fontSize) === 'number' ? fontSize : 12); }; metadataMgr.onChangeLazy(updateIndentSettings); updateIndentSettings(); diff --git a/www/common/translations/messages.js b/www/common/translations/messages.js index 5f46dc982..67873791f 100644 --- a/www/common/translations/messages.js +++ b/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."; diff --git a/www/settings/inner.js b/www/settings/inner.js index 5c167a41a..0e0f12e19 100644 --- a/www/settings/inner.js +++ b/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 = $('
', { + 'class': 'cp-settings-code-font-size cp-sidebarlayout-element' + }); + $('