Keep indentation on Enter in the web UI

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;
         }