Permalink
Browse files

[panel plugin] Make stable option also take effect when a panel is re…

…moved

Issue #4485
  • Loading branch information...
1 parent f78c091 commit 0fb17df6694b0ba63ec0568d84709e9a07e19a9b @marijnh marijnh committed Jan 5, 2017
Showing with 2 additions and 0 deletions.
  1. +2 −0 addon/display/panel.js
@@ -57,6 +57,8 @@
this.cleared = true;
var info = this.cm.state.panels;
this.cm._setSize(null, info.heightLeft += this.height);
+ if (this.options.stable && isAtTop(this.cm, this.node))
+ this.cm.scrollTo(null, this.cm.getScrollInfo().top - this.height)
info.wrapper.removeChild(this.node);
if (--info.panels == 0) removePanels(this.cm);
};

0 comments on commit 0fb17df

Please sign in to comment.