diff --git a/website/src/components/Editor.js b/website/src/components/Editor.js index 89dd596c..02134475 100644 --- a/website/src/components/Editor.js +++ b/website/src/components/Editor.js @@ -79,6 +79,10 @@ export default class Editor extends React.Component { return (this.props.posFromIndex ? this.props : doc).posFromIndex(index); } + _scrollIntoView(doc, pos, margin=0) { + return (this.props.scrollIntoView ? this.props : doc).getEditor().scrollIntoView(pos, margin); + } + componentDidMount() { this._CMHandlers = []; this._subscriptions = []; @@ -167,6 +171,22 @@ export default class Editor extends React.Component { ); } + this._subscriptions.push(subscribe('SCROLL_TO_NODE', ({range}) => { + if (!range) { + return; + } + + let doc = this.codeMirror.getDoc(); + let pos = typeof range[0] == 'number' ? this._posFromIndex(doc, range[0]) : range[0]; + + if (!pos) { + return; + } + + this._scrollIntoView(doc, pos, 200); + }), + ); + if (this.props.error) { this._setError(this.props.error); } diff --git a/website/src/components/visualization/tree/Element.js b/website/src/components/visualization/tree/Element.js index 9e4ec0c3..58e00c0a 100644 --- a/website/src/components/visualization/tree/Element.js +++ b/website/src/components/visualization/tree/Element.js @@ -8,6 +8,7 @@ import focusNodes from '../focusNodes.js' import cx from '../../../utils/classnames.js'; import stringify from '../../../utils/stringify'; +import GotoNode from './GotoNode'; const {useState, useRef, useMemo, useCallback, useEffect} = React; @@ -316,6 +317,7 @@ const Element = React.memo(function Element({ {prefix ? {prefix} : null} {content} {suffix ?