Method decreaseFontSize

src/workspace.js:1912–1917

()

  // Decrease the editor font size by 1px.
  decreaseFontSize() {
    const fontSize = this.config.get('editor.fontSize');
    if (fontSize > 1) {
      this.config.set('editor.fontSize', fontSize - 1);
    }
  }

  // Restore to the window's default editor font size.
  resetFontSize() {