diff --git a/index.html b/index.html
index f633ea8..73f3f23 100644
--- a/index.html
+++ b/index.html
@@ -39,7 +39,7 @@
"bottom files"
"statusbar statusbar";
grid-template-columns: 70% 30%;
- grid-template-rows: 1fr 0.7fr 2.5em;
+ grid-template-rows: auto 1fr 2.5em;
}
.root.fullscreen_editor {
@@ -68,6 +68,8 @@
}
.editor_container {
+ height: 55vh;
+ resize: vertical;
position: relative;
grid-area: code;
font-size: 16px;
diff --git a/src/editor/editor.js b/src/editor/editor.js
index 04665ce..c76b7f1 100644
--- a/src/editor/editor.js
+++ b/src/editor/editor.js
@@ -76,6 +76,8 @@ export class Editor {
this.ui = ui
this.editor_container = editor_container
+ this.make_resizable()
+
this.markers = {}
this.sessions = {}
@@ -468,5 +470,47 @@ export class Editor {
cb(file, this.sessions[file])
}
}
+
+ make_resizable() {
+
+ const apply_height = () => {
+ this.editor_container.style.height = localStorage.editor_height + 'vh'
+ }
+
+ let last_resize_time = new Date().getTime()
+
+ window.addEventListener('resize', () => {
+ last_resize_time = new Date().getTime()
+ })
+
+ // Save editor_height on resize and restore it on reopen
+ if(localStorage.editor_height != null) {
+ apply_height()
+ }
+
+ let is_first_run = true
+
+ new ResizeObserver((e) => {
+ if(is_first_run) {
+ // Resize observer callback seems to fire immediately on create
+ is_first_run = false
+ return
+ }
+ if(new Date().getTime() - last_resize_time < 100) {
+ // Resize observer triggered by window resize, skip
+ return
+ }
+
+ // See https://stackoverflow.com/a/57166828/795038
+ // ace editor must be updated based on container size change
+ this.ace_editor.resize()
+
+ const height = this.editor_container.offsetHeight / window.innerHeight * 100
+ localStorage.editor_height = height
+ // resize applies height in pixels. Wait for it and apply height in vh
+ setTimeout(apply_height, 0)
+
+ }).observe(this.editor_container)
+ }
}