1
1
mirror of https://github.com/Fabio286/antares.git synced 2025-06-05 21:59:22 +02:00

feat(UI): option to change query editors font size, closes #77

This commit is contained in:
2021-06-19 11:54:15 +02:00
parent 3829b94bf7
commit e579f37438
7 changed files with 80 additions and 7 deletions

View File

@ -38,6 +38,7 @@ export default {
computed: {
...mapGetters({
editorTheme: 'settings/getEditorTheme',
editorFontSize: 'settings/getEditorFontSize',
autoComplete: 'settings/getAutoComplete',
lineWrap: 'settings/getLineWrap',
baseCompleter: 'application/getBaseCompleter'
@ -158,6 +159,19 @@ export default {
if (this.editor)
this.editor.setTheme(`ace/theme/${this.editorTheme}`);
},
editorFontSize () {
const sizes = {
small: '12px',
medium: '14px',
large: '16px'
};
if (this.editor) {
this.editor.setOptions({
fontSize: sizes[this.editorFontSize]
});
}
},
autoComplete () {
if (this.editor) {
this.editor.setOptions({