Dynamically stretch the code editor height

webapp/public/js/domjudge.js

@@ -1290,3 +1290,11 @@ function initScoreboardSubmissions() {
         });
     });
 }
+
+function resizeEditors() {
+    // This function assumes that there is at most one tabbed editor in the screen.
+    const activeEditor = document.querySelector(".tab-pane.active .editor");
+    const height = $(window).height() - document.body.offsetHeight + activeEditor.clientHeight - 1 + "px";
+    $('.editor').height(height);
+}
+$(window).resize(resizeEditors);

webapp/public/style_domjudge.css

@@ -754,6 +754,5 @@ blockquote {
 
 .editor {
     width: 100%;
-    height: 80vh;
     border: 1px solid grey;
 }

webapp/src/Twig/TwigExtension.php

@@ -883,6 +883,7 @@ public function codeEditor(
         });
         %s
         %s
+        resizeEditors();
     });
 });
 </script>
@@ -1011,6 +1012,7 @@ public function showDiff(string $id, SubmissionFile $newFile, SubmissionFile $ol
             updateMode(e.target.value);
         });
         updateMode(initialDiffMode);
+        resizeEditors();
     });
 });
 </script>