[FIX] playground: properly resize editors when resizing panels

This commit is contained in:
Géry Debongnie
2019-05-29 22:40:44 +02:00
parent 34b5049dee
commit a554436d03
+7 -6
View File
@@ -314,6 +314,7 @@ class TabbedEditor extends owl.Component {
const session = this.sessions[this.state.currentTab]; const session = this.sessions[this.state.currentTab];
session.setValue(this.props[this.state.currentTab], -1); session.setValue(this.props[this.state.currentTab], -1);
this.editor.setSession(session); this.editor.setSession(session);
this.editor.resize();
} }
willUnmount() { willUnmount() {
@@ -322,12 +323,12 @@ class TabbedEditor extends owl.Component {
} }
setTab(tab) { setTab(tab) {
if (this.state.currentTab !== tab) { if (this.state.currentTab !== tab) {
this.state.currentTab = tab; this.state.currentTab = tab;
const session = this.sessions[this.state.currentTab]; const session = this.sessions[this.state.currentTab];
session.doc.setValue(this.props[tab], -1); session.doc.setValue(this.props[tab], -1);
this.editor.setSession(session); this.editor.setSession(session);
} }
} }
onMouseDown(ev) { onMouseDown(ev) {