From 097767ee2044bcfa8ff030d8210b288e3586dd36 Mon Sep 17 00:00:00 2001 From: yann300 Date: Thu, 4 Apr 2019 11:35:41 +0200 Subject: [PATCH] minwidth for terminal --- src/app/panels/editor-panel.js | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/app/panels/editor-panel.js b/src/app/panels/editor-panel.js index 7dd6652f67..91c4810042 100644 --- a/src/app/panels/editor-panel.js +++ b/src/app/panels/editor-panel.js @@ -79,10 +79,9 @@ class EditorPanel { self._view.mainPanel.style.display = 'none' }) self.data = { - _FILE_SCROLL_DELTA: 200, _layout: { top: { - offset: self._deps.config.get('terminal-top-offset') || 500, + offset: self._deps.config.get('terminal-top-offset') || 150, show: true } } @@ -104,7 +103,7 @@ class EditorPanel { var height = window.innerHeight var newpos = (event.pageY < limitUp) ? limitUp : event.pageY newpos = (newpos < height - limitDown) ? newpos : height - limitDown - return newpos + return height - newpos } }) @@ -138,11 +137,11 @@ class EditorPanel { var tmp = delta - limitDown delta = tmp > 0 ? tmp : 0 if (direction === 'top') { - var height = containerHeight - delta - height = height < 0 ? 0 : height - self._view.editor.style.height = `${delta}px` - self._view.mainPanel.style.height = `${delta}px` - self._view.terminal.style.height = `${height}px` // - menu bar height + var mainPanelHeight = containerHeight - delta + mainPanelHeight = mainPanelHeight < 0 ? 0 : mainPanelHeight + self._view.editor.style.height = `${mainPanelHeight}px` + self._view.mainPanel.style.height = `${mainPanelHeight}px` + self._view.terminal.style.height = `${delta}px` // - menu bar height self._components.editor.resize((document.querySelector('#editorWrap') || {}).checked) self._components.terminal.scroll2bottom() }