refactor(frontend): editor theme improvements

3 files changed, 370 insertions, 10 deletions

diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts
index fa77862c..325f8d18 100644
--- a/subprojects/frontend/src/editor/EditorTheme.ts
+++ b/subprojects/frontend/src/editor/EditorTheme.ts
@@ -4,6 +4,11 @@ import infoSVG from '@material-icons/svg/svg/info/baseline.svg?raw';
 import warningSVG from '@material-icons/svg/svg/warning/baseline.svg?raw';
 import { alpha, styled, type CSSObject } from '@mui/material/styles';
 
+import {
+  INDENTATION_MARKER_ACTIVE_CLASS,
+  INDENTATION_MARKER_CLASS,
+} from './indentationMarkerViewPlugin';
+
 function svgURL(svg: string): string {
   return `url('data:image/svg+xml;utf8,${svg}')`;
 }
@@ -62,6 +67,9 @@ export default styled('div', {
         background: theme.palette.highlight.selection,
       },
     },
+    '.cm-line': {
+      position: 'relative', // For indentation highlights
+    },
   };
 
   const highlightingStyle: CSSObject = {
@@ -149,6 +157,13 @@ export default styled('div', {
     '.cm-searchMatch-selected': {
       background: theme.palette.highlight.search.selected,
     },
+    [`.${INDENTATION_MARKER_CLASS}`]: {
+      display: 'inline-block',
+      boxShadow: `1px 0 0 ${theme.palette.highlight.lineNumber} inset`,
+    },
+    [`.${INDENTATION_MARKER_CLASS}.${INDENTATION_MARKER_ACTIVE_CLASS}`]: {
+      boxShadow: `1px 0 0 ${theme.palette.text.primary} inset`,
+    },
   };
 
   const lineNumberStyle: CSSObject = {
@@ -311,17 +326,7 @@ export default styled('div', {
 
   const foldStyle = {
     '.cm-foldGutter': {
-      opacity: 0,
       width: 16,
-      transition: theme.transitions.create('opacity', {
-        duration: theme.transitions.duration.short,
-      }),
-      '@media (hover: none)': {
-        opacity: 1,
-      },
-    },
-    '.cm-gutters:hover .cm-foldGutter': {
-      opacity: 1,
     },
     '.problem-editor-foldMarker': {
       display: 'block',
@@ -338,6 +343,18 @@ export default styled('div', {
         margin: '2px 0',
       },
     },
+    '.problem-editor-foldMarker-open': {
+      opacity: 0,
+      transition: theme.transitions.create('opacity', {
+        duration: theme.transitions.duration.short,
+      }),
+      '@media (hover: none)': {
+        opacity: 1,
+      },
+    },
+    '.cm-gutters:hover .problem-editor-foldMarker-open': {
+      opacity: 1,
+    },
     '.problem-editor-foldMarker-closed': {
       transform: 'rotate(-90deg)',
     },
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts
index c61f4a22..079e8a47 100644
--- a/subprojects/frontend/src/editor/createEditorState.ts
+++ b/subprojects/frontend/src/editor/createEditorState.ts
@@ -37,6 +37,7 @@ import problemLanguageSupport from '../language/problemLanguageSupport';
 import type EditorStore from './EditorStore';
 import SearchPanel from './SearchPanel';
 import findOccurrences from './findOccurrences';
+import indentationMarkerViewPlugin from './indentationMarkerViewPlugin';
 import semanticHighlighting from './semanticHighlighting';
 
 export default function createEditorState(
@@ -60,6 +61,7 @@ export default function createEditorState(
       highlightSpecialChars(),
       history(),
       indentOnInput(),
+      indentationMarkerViewPlugin(),
       rectangularSelection(),
       search({
         createPanel(view) {
diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts
new file mode 100644
index 00000000..96be0eea
--- /dev/null
+++ b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts
@@ -0,0 +1,341 @@
+/**
+ * @file CodeMirror plugin to highlight indentation
+ *
+ * This file is based on the
+ * [@replit/codemirror-indentation-markers](https://github.com/replit/codemirror-indentation-markers)
+ * package, which is available under the
+ * [MIT License](https://github.com/replit/codemirror-indentation-markers/blob/543cc508ca5cef5d8350af23973eb1425e31525c/LICENSE).
+ *
+ * The highlighting heuristics were adjusted to make them more suitable
+ * for logic programming.
+ *
+ * @see https://github.com/replit/codemirror-indentation-markers/blob/543cc508ca5cef5d8350af23973eb1425e31525c/src/index.ts
+ */
+
+import { getIndentUnit } from '@codemirror/language';
+import { Text, RangeSet, EditorState } from '@codemirror/state';
+import {
+  ViewPlugin,
+  Decoration,
+  EditorView,
+  WidgetType,
+  PluginValue,
+} from '@codemirror/view';
+
+export const INDENTATION_MARKER_CLASS = 'cm-indentation-marker';
+
+export const INDENTATION_MARKER_ACTIVE_CLASS = 'active';
+
+const indentationMark = Decoration.mark({
+  class: INDENTATION_MARKER_CLASS,
+  tagName: 'span',
+});
+
+const activeIndentationMark = Decoration.mark({
+  class: `${INDENTATION_MARKER_CLASS} ${INDENTATION_MARKER_ACTIVE_CLASS}`,
+  tagName: 'span',
+});
+
+/**
+ * Widget used to simulate N indentation markers on empty lines.
+ */
+class IndentationWidget extends WidgetType {
+  constructor(
+    readonly numIndent: number,
+    readonly indentSize: number,
+    readonly activeIndent?: number,
+  ) {
+    super();
+  }
+
+  override eq(other: IndentationWidget) {
+    return (
+      this.numIndent === other.numIndent &&
+      this.indentSize === other.indentSize &&
+      this.activeIndent === other.activeIndent
+    );
+  }
+
+  override toDOM(view: EditorView) {
+    const indentSize = getIndentUnit(view.state);
+
+    const wrapper = document.createElement('span');
+    wrapper.style.top = '0';
+    wrapper.style.left = '4px';
+    wrapper.style.position = 'absolute';
+    wrapper.style.pointerEvents = 'none';
+
+    for (let indent = 0; indent < this.numIndent; indent += 1) {
+      const element = document.createElement('span');
+      element.className = INDENTATION_MARKER_CLASS;
+      element.classList.toggle(
+        INDENTATION_MARKER_ACTIVE_CLASS,
+        indent === this.activeIndent,
+      );
+      element.innerHTML = ' '.repeat(indentSize);
+      wrapper.appendChild(element);
+    }
+
+    return wrapper;
+  }
+}
+
+/**
+ * Returns the number of indentation markers a non-empty line should have
+ * based on the text in the line and the size of the indent.
+ */
+function getNumIndentMarkersForNonEmptyLine(
+  text: string,
+  indentSize: number,
+  onIndentMarker?: (pos: number) => void,
+) {
+  let numIndents = 0;
+  let numConsecutiveSpaces = 0;
+  let prevChar: string | null = null;
+
+  for (let char = 0; char < text.length; char += 1) {
+    // Bail if we encounter a non-whitespace character
+    if (text[char] !== ' ' && text[char] !== '\t') {
+      // We still increment the indentation level if we would
+      // have added a marker here had this been a space or tab.
+      if (numConsecutiveSpaces % indentSize === 0 && char !== 0) {
+        numIndents += 1;
+      }
+
+      return numIndents;
+    }
+
+    // Every tab and N space has an indentation marker
+    const shouldAddIndent =
+      prevChar === '\t' || numConsecutiveSpaces % indentSize === 0;
+
+    if (shouldAddIndent) {
+      numIndents += 1;
+
+      if (onIndentMarker) {
+        onIndentMarker(char);
+      }
+    }
+
+    if (text[char] === ' ') {
+      numConsecutiveSpaces += 1;
+    } else {
+      numConsecutiveSpaces = 0;
+    }
+
+    prevChar = text[char];
+  }
+
+  return numIndents;
+}
+
+/**
+ * Returns the number of indent markers an empty line should have
+ * based on the number of indent markers of the previous
+ * and next non-empty lines.
+ */
+function getNumIndentMarkersForEmptyLine(prev: number, next: number) {
+  const min = Math.min(prev, next);
+  const max = Math.max(prev, next);
+
+  // If only one side is non-zero, we omit markers,
+  // because in logic programming, a block often ends with an empty line.
+  if (min === 0 && max > 0) {
+    return 0;
+  }
+
+  // Else, default to the minimum of the two
+  return min;
+}
+
+/**
+ * Returns the next non-empty line and its indent level.
+ */
+function findNextNonEmptyLineAndIndentLevel(
+  doc: Text,
+  startLine: number,
+  indentSize: number,
+): [number, number] {
+  const numLines = doc.lines;
+  let lineNo = startLine;
+
+  while (lineNo <= numLines) {
+    const { text } = doc.line(lineNo);
+
+    if (text.trim().length === 0) {
+      lineNo += 1;
+    } else {
+      const indent = getNumIndentMarkersForNonEmptyLine(text, indentSize);
+      return [lineNo, indent];
+    }
+  }
+
+  // Reached the end of the doc
+  return [numLines + 1, 0];
+}
+
+interface IndentationMarkerDesc {
+  lineNumber: number;
+  from: number;
+  to: number;
+  create(activeIndentIndex?: number): Decoration;
+}
+
+/**
+ * Returns a range of lines with an active indent marker.
+ */
+function getLinesWithActiveIndentMarker(
+  state: EditorState,
+  indentMap: Map<number, number>,
+): { start: number; end: number; activeIndent: number } {
+  const currentLine = state.doc.lineAt(state.selection.main.head);
+  const currentIndent = indentMap.get(currentLine.number);
+  const currentLineNo = currentLine.number;
+
+  if (!currentIndent) {
+    return { start: -1, end: -1, activeIndent: NaN };
+  }
+
+  let start: number;
+  let end: number;
+
+  for (start = currentLineNo; start >= 0; start -= 1) {
+    const indent = indentMap.get(start - 1);
+    if (!indent || indent < currentIndent) {
+      break;
+    }
+  }
+
+  for (end = currentLineNo; ; end += 1) {
+    const indent = indentMap.get(end + 1);
+    if (!indent || indent < currentIndent) {
+      break;
+    }
+  }
+
+  return { start, end, activeIndent: currentIndent };
+}
+/**
+ * Adds indentation markers to all lines within view.
+ */
+function addIndentationMarkers(view: EditorView) {
+  const indentSize = getIndentUnit(view.state);
+  const indentSizeMap = new Map</* lineNumber */ number, number>();
+  const decorations: Array<IndentationMarkerDesc> = [];
+
+  view.visibleRanges.forEach(({ from, to }) => {
+    let pos = from;
+
+    let prevIndentMarkers = 0;
+    let nextIndentMarkers = 0;
+    let nextNonEmptyLine = 0;
+
+    while (pos <= to) {
+      const line = view.state.doc.lineAt(pos);
+      const { text } = line;
+
+      // If a line is empty, we match the indentation according
+      // to a heuristic based on the indentations of the
+      // previous and next non-empty lines.
+      if (text.trim().length === 0) {
+        // To retrieve the next non-empty indentation level,
+        // we perform a lookahead and cache the result.
+        if (nextNonEmptyLine < line.number) {
+          const [nextLine, nextIndent] = findNextNonEmptyLineAndIndentLevel(
+            view.state.doc,
+            line.number + 1,
+            indentSize,
+          );
+
+          nextNonEmptyLine = nextLine;
+          nextIndentMarkers = nextIndent;
+        }
+
+        const numIndentMarkers = getNumIndentMarkersForEmptyLine(
+          prevIndentMarkers,
+          nextIndentMarkers,
+        );
+
+        // Add the indent widget and move on to next line
+        indentSizeMap.set(line.number, numIndentMarkers);
+        decorations.push({
+          from: pos,
+          to: pos,
+          lineNumber: line.number,
+          create: (activeIndentIndex) =>
+            Decoration.widget({
+              widget: new IndentationWidget(
+                numIndentMarkers,
+                indentSize,
+                activeIndentIndex,
+              ),
+            }),
+        });
+      } else {
+        const indices: Array<number> = [];
+
+        prevIndentMarkers = getNumIndentMarkersForNonEmptyLine(
+          text,
+          indentSize,
+          (char) => indices.push(char),
+        );
+
+        indentSizeMap.set(line.number, indices.length);
+        decorations.push(
+          ...indices.map(
+            (char, i): IndentationMarkerDesc => ({
+              from: line.from + char,
+              to: line.from + char + 1,
+              lineNumber: line.number,
+              create: (activeIndentIndex) =>
+                activeIndentIndex === i
+                  ? activeIndentationMark
+                  : indentationMark,
+            }),
+          ),
+        );
+      }
+
+      // Move on to the next line
+      pos = line.to + 1;
+    }
+  });
+
+  const activeBlockRange = getLinesWithActiveIndentMarker(
+    view.state,
+    indentSizeMap,
+  );
+
+  return RangeSet.of<Decoration>(
+    Array.from(decorations).map(({ lineNumber, from, to, create }) => {
+      const activeIndent =
+        lineNumber >= activeBlockRange.start &&
+        lineNumber <= activeBlockRange.end
+          ? activeBlockRange.activeIndent - 1
+          : undefined;
+
+      return { from, to, value: create(activeIndent) };
+    }),
+    true,
+  );
+}
+
+export default function indentationMarkerViewPlugin() {
+  return ViewPlugin.define<PluginValue & { decorations: RangeSet<Decoration> }>(
+    (view) => ({
+      decorations: addIndentationMarkers(view),
+      update(update) {
+        if (
+          update.docChanged ||
+          update.viewportChanged ||
+          update.selectionSet
+        ) {
+          this.decorations = addIndentationMarkers(update.view);
+        }
+      },
+    }),
+    {
+      decorations: (v) => v.decorations,
+    },
+  );
+}