From 67b271b1fa39719f69154d68ba660770b86e189e Mon Sep 17 00:00:00 2001 From: Alexey Korepanov Date: Wed, 1 Mar 2023 12:20:49 +0100 Subject: [PATCH] Keep indentation on Enter in the web UI --- programs/server/play.html | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/programs/server/play.html b/programs/server/play.html index c511d13cf91..d90293fbd1b 100644 --- a/programs/server/play.html +++ b/programs/server/play.html @@ -669,6 +669,29 @@ elem.selectionStart = selection_start + 4; elem.selectionEnd = selection_start + 4; + e.preventDefault(); + return false; + } else if (e.key === 'Enter') { + // If the user presses Enter, and the previous line starts with spaces, + // then we will insert the same number of spaces. + const elem = e.target; + if (elem.selectionStart !== elem.selectionEnd) { + // If there is a selection, then we will not insert spaces. + return; + } + const cursor_pos = elem.selectionStart; + + const elem_value = elem.value; + const text_before_cursor = elem_value.substring(0, cursor_pos); + const text_after_cursor = elem_value.substring(cursor_pos); + const prev_lines = text_before_cursor.split('\n'); + const prev_line = prev_lines.pop(); + const lead_spaces = prev_line.match(/^\s*/)[0]; + // Add leading spaces to the current line. + elem.value = text_before_cursor + '\n' + lead_spaces + text_after_cursor; + elem.selectionStart = cursor_pos + lead_spaces.length + 1; + elem.selectionEnd = elem.selectionStart; + e.preventDefault(); return false; }