From a854b1acdef27c54fe008d236282386efc44783e Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 26 Apr 2023 20:01:20 +0200 Subject: fix(web): editor cursor styling Temporarily remove custom scrollbar and indentation styling, because they interferred with cursor visibility. --- subprojects/frontend/src/editor/EditorTheme.ts | 126 +------ .../frontend/src/editor/createEditorState.ts | 4 - .../src/editor/indentationMarkerViewPlugin.ts | 347 -------------------- .../frontend/src/editor/scrollbarViewPlugin.ts | 363 --------------------- 4 files changed, 3 insertions(+), 837 deletions(-) delete mode 100644 subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts delete mode 100644 subprojects/frontend/src/editor/scrollbarViewPlugin.ts (limited to 'subprojects/frontend/src/editor') diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index 023a8f73..e057ce18 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts @@ -14,32 +14,6 @@ function svgURL(svg: string): string { return `url('data:image/svg+xml;utf8,${svg}')`; } -function radialShadowTheme( - origin: string, - scaleX: boolean, - scaleY: boolean, -): CSSObject { - function radialGradient(opacity: number, scale: string): string { - return `radial-gradient( - farthest-side at ${origin}, - rgba(0, 0, 0, ${opacity}), - rgba(0, 0, 0, 0) - ) - ${origin} / - ${scaleX ? scale : '100%'} - ${scaleY ? scale : '100%'} - no-repeat`; - } - - return { - background: ` - ${radialGradient(0.2, '40%')}, - ${radialGradient(0.14, '50%')}, - ${radialGradient(0.12, '100%')} - `, - }; -} - export default styled('div', { name: 'EditorTheme', shouldForwardProp: (propName) => @@ -58,98 +32,13 @@ export default styled('div', { }, }; - const scrollerThumbOpacity = theme.palette.mode === 'dark' ? 0.16 : 0.28; - const generalStyle: CSSObject = { background: theme.palette.background.default, '&, .cm-editor': { height: '100%', }, - '.cm-scroller-holder': { - display: 'flex', - position: 'relative', - flexDirection: 'column', - overflow: 'hidden', - flex: '1 1', - }, - '.cm-scroller-spacer': { - position: 'sticky', - flexShrink: 0, - zIndex: 300, - width: 1, - marginRight: -1, - pointerEvents: 'none', - }, '.cm-scroller': { color: theme.palette.text.secondary, - scrollbarWidth: 'none', - MsOverflowStyle: 'none', - '&::-webkit-scrollbar': { - width: 0, - height: 0, - background: 'transparent', - }, - }, - '.cm-scroller-track': { - position: 'absolute', - zIndex: 300, - touchAction: 'none', - }, - '.cm-scroller-thumb': { - position: 'absolute', - background: theme.palette.text.secondary, - opacity: scrollerThumbOpacity, - transition: theme.transitions.create('opacity', { - duration: theme.transitions.duration.shortest, - }), - touchAction: 'none', - WebkitTapHighlightColor: 'transparent', - '&:hover': { - opacity: 0.75, - '@media (hover: none)': { - opacity: scrollerThumbOpacity, - }, - }, - '&.active': { - opacity: 1, - pointerEvents: 'none', - userSelect: 'none', - }, - }, - '.cm-scroller-track-y, .cm-scroller-thumb-y': { - top: 0, - right: 0, - width: 12, - }, - '.cm-scroller-track-x, .cm-scroller-thumb-x': { - left: 0, - bottom: 0, - height: 12, - }, - '.cm-scroller-track-x': { - right: 12, - }, - '.cm-scroller-gutter-decoration': { - position: 'absolute', - top: 0, - bottom: 0, - left: 0, - width: 0, - transition: theme.transitions.create('width', { - duration: theme.transitions.duration.shortest, - }), - ...radialShadowTheme('0 50%', true, false), - }, - '.cm-scroller-top-decoration': { - position: 'absolute', - top: 0, - left: 0, - right: 0, - height: 0, - transition: theme.transitions.create('height', { - duration: theme.transitions.duration.shortest, - }), - ...radialShadowTheme('50% 0', false, true), }, '.cm-gutters': { background: theme.palette.background.default, @@ -168,7 +57,6 @@ export default styled('div', { background: 'transparent', }, '.cm-cursor, .cm-cursor-primary': { - marginLeft: -1, borderLeft: `2px solid ${theme.palette.info.main}`, }, '.cm-selectionBackground': { @@ -181,7 +69,6 @@ export default styled('div', { }, }, '.cm-line': { - position: 'relative', // For indentation highlights padding: '0 12px 0 0px', }, }; @@ -271,13 +158,6 @@ export default styled('div', { '.cm-searchMatch-selected': { background: theme.palette.highlight.search.selected, }, - '.cm-indentation-marker': { - display: 'inline-block', - boxShadow: `1px 0 0 ${theme.palette.text.disabled} inset`, - '&.active': { - boxShadow: `1px 0 0 ${theme.palette.text.primary} inset`, - }, - }, '.cm-scroller-selection': { position: 'absolute', right: 0, @@ -458,11 +338,11 @@ export default styled('div', { const foldStyle = { '.cm-foldGutter': { - width: 17, + width: 16, }, '.problem-editor-foldMarker': { display: 'block', - margin: '4px 1px 4px 0', + margin: '4px 0 4px 0', padding: 0, maskImage: svgURL(expandMoreSVG), maskSize: '16px 16px', @@ -473,7 +353,7 @@ export default styled('div', { cursor: 'pointer', WebkitTapHighlightColor: 'transparent', [theme.breakpoints.down('sm')]: { - margin: '2px 1px 2px 0', + margin: '2px 0 2px 0', }, }, '.problem-editor-foldMarker-open': { diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts index 4a8e9832..67b8fb9e 100644 --- a/subprojects/frontend/src/editor/createEditorState.ts +++ b/subprojects/frontend/src/editor/createEditorState.ts @@ -44,8 +44,6 @@ import type EditorStore from './EditorStore'; import SearchPanel from './SearchPanel'; import exposeDiagnostics from './exposeDiagnostics'; import findOccurrences from './findOccurrences'; -import indentationMarkerViewPlugin from './indentationMarkerViewPlugin'; -import scrollbarViewPlugin from './scrollbarViewPlugin'; import semanticHighlighting from './semanticHighlighting'; export default function createEditorState( @@ -70,7 +68,6 @@ export default function createEditorState( highlightSpecialChars(), history(), indentOnInput(), - indentationMarkerViewPlugin(), rectangularSelection(), search({ createPanel(view) { @@ -129,7 +126,6 @@ export default function createEditorState( ...defaultKeymap, ]), problemLanguageSupport(), - scrollbarViewPlugin(store), ], }); } diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts deleted file mode 100644 index 57a946d5..00000000 --- a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts +++ /dev/null @@ -1,347 +0,0 @@ -/* - * 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(); - 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, - }, - ); -} diff --git a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts b/subprojects/frontend/src/editor/scrollbarViewPlugin.ts deleted file mode 100644 index 878d369d..00000000 --- a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts +++ /dev/null @@ -1,363 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ - -import { EditorSelection } from '@codemirror/state'; -import { - type EditorView, - type PluginValue, - ViewPlugin, -} from '@codemirror/view'; -import { reaction } from 'mobx'; - -import type EditorStore from './EditorStore'; -import { getDiagnostics } from './exposeDiagnostics'; -import findOccurrences from './findOccurrences'; - -export const HOLDER_CLASS = 'cm-scroller-holder'; -export const SPACER_CLASS = 'cm-scroller-spacer'; -export const TRACK_CLASS = 'cm-scroller-track'; -export const THUMB_CLASS = 'cm-scroller-thumb'; -export const THUMB_ACTIVE_CLASS = 'active'; -export const GUTTER_DECORATION_CLASS = 'cm-scroller-gutter-decoration'; -export const TOP_DECORATION_CLASS = 'cm-scroller-top-decoration'; -export const ANNOTATION_SELECTION_CLASS = 'cm-scroller-selection'; -export const ANNOTATION_DIAGNOSTIC_CLASS = 'cm-scroller-diagnostic'; -export const ANNOTATION_OCCURRENCE_CLASS = 'cm-scroller-occurrence'; -export const SHADOW_WIDTH = 10; -export const SCROLLBAR_WIDTH = 12; -export const ANNOTATION_WIDTH = SCROLLBAR_WIDTH / 2; -export const MIN_ANNOTATION_HEIGHT = 1; - -function createScrollbar( - holder: HTMLElement, - direction: 'x' | 'y', - touchCallback: (offsetX: number, offsetY: number) => void, - moveCallback: (movementX: number, movementY: number) => void, -): { track: HTMLElement; thumb: HTMLElement } { - const track = holder.ownerDocument.createElement('div'); - track.className = `${TRACK_CLASS} ${TRACK_CLASS}-${direction}`; - holder.appendChild(track); - - const thumb = holder.ownerDocument.createElement('div'); - thumb.className = `${THUMB_CLASS} ${THUMB_CLASS}-${direction}`; - track.appendChild(thumb); - - let pointerId: number | undefined; - track.addEventListener('pointerdown', (event) => { - if (pointerId !== undefined) { - event.preventDefault(); - return; - } - ({ pointerId } = event); - thumb.classList.add(THUMB_ACTIVE_CLASS); - if (event.target === thumb) { - // Prevent implicit pointer capture on mobile. - thumb.releasePointerCapture(pointerId); - } else { - touchCallback(event.offsetX, event.offsetY); - } - track.setPointerCapture(pointerId); - }); - - track.addEventListener('pointermove', (event) => { - if (event.pointerId !== pointerId) { - return; - } - moveCallback(event.movementX, event.movementY); - event.preventDefault(); - }); - - function scrollEnd(event: PointerEvent) { - if (event.pointerId !== pointerId) { - return; - } - pointerId = undefined; - thumb.classList.remove(THUMB_ACTIVE_CLASS); - } - - track.addEventListener('pointerup', scrollEnd, { passive: true }); - track.addEventListener('pointercancel', scrollEnd, { passive: true }); - - return { track, thumb }; -} - -function rebuildAnnotations( - view: EditorView, - scrollHeight: number, - trackYHeight: number, - holder: HTMLElement, - annotations: HTMLDivElement[], -) { - const { state } = view; - const overlayAnnotationsHeight = - (view.contentHeight / scrollHeight) * trackYHeight; - const lineHeight = overlayAnnotationsHeight / state.doc.lines; - - let i = 0; - - function getOrCreateAnnotation(from: number, to?: number): HTMLDivElement { - const startLine = state.doc.lineAt(from).number; - const endLine = to === undefined ? startLine : state.doc.lineAt(to).number; - const top = (startLine - 1) * lineHeight; - const height = Math.max( - MIN_ANNOTATION_HEIGHT, - Math.max(1, endLine - startLine) * lineHeight, - ); - - let annotation: HTMLDivElement | undefined; - if (i < annotations.length) { - annotation = annotations[i]; - } - if (annotation === undefined) { - annotation = holder.ownerDocument.createElement('div'); - annotations.push(annotation); - holder.appendChild(annotation); - } - i += 1; - - annotation.style.top = `${top}px`; - annotation.style.height = `${height}px`; - - return annotation; - } - - state.selection.ranges.forEach(({ head }) => { - const selectionAnnotation = getOrCreateAnnotation(head); - selectionAnnotation.className = ANNOTATION_SELECTION_CLASS; - selectionAnnotation.style.width = `${SCROLLBAR_WIDTH}px`; - }); - - const diagnosticsIter = getDiagnostics(state).iter(); - while (diagnosticsIter.value !== null) { - const diagnosticAnnotation = getOrCreateAnnotation( - diagnosticsIter.from, - diagnosticsIter.to, - ); - diagnosticAnnotation.className = `${ANNOTATION_DIAGNOSTIC_CLASS} ${ANNOTATION_DIAGNOSTIC_CLASS}-${diagnosticsIter.value.severity}`; - diagnosticAnnotation.style.width = `${ANNOTATION_WIDTH}px`; - diagnosticsIter.next(); - } - - const occurrences = view.state.field(findOccurrences); - const occurrencesIter = occurrences.iter(); - while (occurrencesIter.value !== null) { - const occurrenceAnnotation = getOrCreateAnnotation( - occurrencesIter.from, - occurrencesIter.to, - ); - occurrenceAnnotation.className = ANNOTATION_OCCURRENCE_CLASS; - occurrenceAnnotation.style.width = `${ANNOTATION_WIDTH}px`; - occurrenceAnnotation.style.right = `${ANNOTATION_WIDTH}px`; - occurrencesIter.next(); - } - - annotations - .splice(i) - .forEach((staleAnnotation) => holder.removeChild(staleAnnotation)); -} - -export default function scrollbarViewPlugin( - editorStore: EditorStore, -): ViewPlugin { - return ViewPlugin.define((view) => { - const { scrollDOM } = view; - const { ownerDocument, parentElement: parentDOM } = scrollDOM; - if (parentDOM === null) { - return {}; - } - - const holder = ownerDocument.createElement('div'); - holder.className = HOLDER_CLASS; - parentDOM.replaceChild(holder, scrollDOM); - holder.appendChild(scrollDOM); - - const spacer = ownerDocument.createElement('div'); - spacer.className = SPACER_CLASS; - scrollDOM.insertBefore(spacer, scrollDOM.firstChild); - - let gutterWidth = 0; - - scrollDOM.addEventListener('click', (event) => { - const scrollX = scrollDOM.scrollLeft + event.offsetX; - const scrollY = scrollDOM.scrollTop + event.offsetY; - if (scrollX > gutterWidth && scrollY > view.contentHeight) { - event.preventDefault(); - view.focus(); - editorStore.dispatch({ - scrollIntoView: true, - selection: EditorSelection.create([ - EditorSelection.cursor(view.state.doc.length), - ]), - }); - } - }); - - let factorY = 1; - let factorX = 1; - - const { track: trackY, thumb: thumbY } = createScrollbar( - holder, - 'y', - (_offsetX, offsetY) => { - const scaledOffset = offsetY / factorY; - const { height: scrollerHeight } = scrollDOM.getBoundingClientRect(); - const target = Math.max(0, scaledOffset - scrollerHeight / 2); - scrollDOM.scrollTo({ top: target }); - }, - (_movementX, movementY) => { - scrollDOM.scrollBy({ top: movementY / factorY }); - }, - ); - - const { track: trackX, thumb: thumbX } = createScrollbar( - holder, - 'x', - (offsetX) => { - const scaledOffset = offsetX / factorX; - const { width: scrollerWidth } = scrollDOM.getBoundingClientRect(); - const target = Math.max(0, scaledOffset - scrollerWidth / 2); - scrollDOM.scrollTo({ left: target }); - }, - (movementX) => { - scrollDOM.scrollBy({ left: movementX / factorX }); - }, - ); - - const gutterDecoration = ownerDocument.createElement('div'); - gutterDecoration.className = GUTTER_DECORATION_CLASS; - holder.appendChild(gutterDecoration); - - const topDecoration = ownerDocument.createElement('div'); - topDecoration.className = TOP_DECORATION_CLASS; - holder.appendChild(topDecoration); - - const disposePanelReaction = reaction( - () => editorStore.searchPanel.state, - (panelOpen) => { - topDecoration.style.display = panelOpen ? 'none' : 'block'; - }, - { fireImmediately: true }, - ); - - let gutters: Element | undefined; - - let firstRun = true; - let firstRunTimeout: number | undefined; - let requested = false; - let rebuildRequested = false; - - const annotations: HTMLDivElement[] = []; - - let observer: ResizeObserver | undefined; - - function update() { - requested = false; - - if (gutters === undefined) { - gutters = scrollDOM.querySelector('.cm-gutters') ?? undefined; - if (gutters !== undefined && observer !== undefined) { - observer.observe(gutters); - } - } - - const { height: scrollerHeight, width: scrollerWidth } = - scrollDOM.getBoundingClientRect(); - const { scrollTop, scrollLeft, scrollWidth } = scrollDOM; - const scrollHeight = - view.contentHeight + scrollerHeight - view.defaultLineHeight; - if (firstRun) { - if (firstRunTimeout !== undefined) { - clearTimeout(firstRunTimeout); - } - firstRunTimeout = setTimeout(() => { - spacer.style.minHeight = `${scrollHeight}px`; - firstRun = false; - }, 0); - } else { - spacer.style.minHeight = `${scrollHeight}px`; - } - gutterWidth = gutters?.clientWidth ?? 0; - let trackYHeight = scrollerHeight; - - // Prevent spurious horizontal scrollbar by rounding up to the nearest pixel. - if (scrollWidth > Math.ceil(scrollerWidth)) { - // Leave space for horizontal scrollbar. - trackYHeight -= SCROLLBAR_WIDTH; - // Alwalys leave space for annotation in the vertical scrollbar. - const trackXWidth = scrollerWidth - gutterWidth - SCROLLBAR_WIDTH; - const thumbWidth = trackXWidth * (scrollerWidth / scrollWidth); - factorX = (trackXWidth - thumbWidth) / (scrollWidth - scrollerWidth); - trackY.style.bottom = `${SCROLLBAR_WIDTH}px`; - trackX.style.display = 'block'; - trackX.style.left = `${gutterWidth}px`; - thumbX.style.width = `${thumbWidth}px`; - thumbX.style.left = `${scrollLeft * factorX}px`; - scrollDOM.style.overflowX = 'scroll'; - } else { - trackY.style.bottom = '0px'; - trackX.style.display = 'none'; - scrollDOM.style.overflowX = 'hidden'; - } - - const thumbHeight = trackYHeight * (scrollerHeight / scrollHeight); - factorY = (trackYHeight - thumbHeight) / (scrollHeight - scrollerHeight); - thumbY.style.display = 'block'; - thumbY.style.height = `${thumbHeight}px`; - thumbY.style.top = `${scrollTop * factorY}px`; - - gutterDecoration.style.left = `${gutterWidth}px`; - gutterDecoration.style.width = `${Math.max( - 0, - Math.min(scrollLeft, SHADOW_WIDTH), - )}px`; - - topDecoration.style.height = `${Math.max( - 0, - Math.min(scrollTop, SHADOW_WIDTH), - )}px`; - - if (rebuildRequested) { - rebuildAnnotations( - view, - scrollHeight, - trackYHeight, - holder, - annotations, - ); - rebuildRequested = false; - } - } - - function requestUpdate() { - if (!requested) { - requested = true; - view.requestMeasure({ read: update }); - } - } - - function requestRebuild() { - requestUpdate(); - rebuildRequested = true; - } - - observer = new ResizeObserver(requestRebuild); - observer.observe(holder); - - scrollDOM.addEventListener('scroll', requestUpdate); - - requestRebuild(); - - return { - update: requestRebuild, - destroy() { - disposePanelReaction(); - observer?.disconnect(); - scrollDOM.removeEventListener('scroll', requestUpdate); - parentDOM.replaceChild(holder, holder); - }, - }; - }); -} -- cgit v1.2.3-70-g09d2