From 823170312ae8362b248462964ba1960a5e7b8c49 Mon Sep 17 00:00:00 2001
From: Dmitry Vasilev <dmitry.vasil@gmail.com>
Date: Tue, 4 Jul 2023 20:24:42 +0300
Subject: [PATCH] resize editor

---
 index.html           |  4 +++-
 src/editor/editor.js | 44 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 1 deletion(-)

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)
+  }
 }