/*
* Copyright (c) 2022 Replit
* Copyright (c) 2022-2023 The Refinery Authors
*
* SPDX-License-Identifier: MIT OR EPL-2.0
*/
/**
* @file CodeMirror plugin to highlight indentation
*
* This file is based on the
* [@replit/codemirror-indentation-markers](https://github.com/replit/codemirror-indentation-markers)
* package.
*
* 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 = '0';
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 | undefined;
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,
): { 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 = [];
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 = [];
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(
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 }>(
(view) => ({
decorations: addIndentationMarkers(view),
update(update) {
if (
update.docChanged ||
update.viewportChanged ||
update.selectionSet
) {
this.decorations = addIndentationMarkers(update.view);
}
},
}),
{
decorations: (v) => v.decorations,
},
);
}