diff options
Diffstat (limited to '')
| -rw-r--r-- | public/js/index.js | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/public/js/index.js b/public/js/index.js index c6a4f770..6e13fe9c 100644 --- a/public/js/index.js +++ b/public/js/index.js @@ -566,7 +566,10 @@ var previousFocusOnEditor = null function checkEditorStyle () { var desireHeight = editorInstance.statusBar ? (ui.area.edit.height() - editorInstance.statusBar.outerHeight()) : ui.area.edit.height() - // set editor height and min height based on scrollbar style and mode + if (editorInstance.toolBar) { + desireHeight = desireHeight - editorInstance.toolBar.outerHeight() + } + // set editor height and min height based on scrollbar style and mode var scrollbarStyle = editor.getOption('scrollbarStyle') if (scrollbarStyle === 'overlay' || appState.currentMode === modeType.both) { ui.area.codemirrorScroll.css('height', desireHeight + 'px') @@ -804,6 +807,10 @@ function changeMode (type) { editorInstance.addStatusBar() editorInstance.updateStatusBar() } + // add and update tool bar + if (!editorInstance.toolBar) { + editorInstance.addToolBar() + } // work around foldGutter might not init properly editor.setOption('foldGutter', false) editor.setOption('foldGutter', true) |