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 ?
{suffix}
: null} + ); }, diff --git a/website/src/components/visualization/tree/GotoNode.js b/website/src/components/visualization/tree/GotoNode.js new file mode 100644 index 00000000..736abe6b --- /dev/null +++ b/website/src/components/visualization/tree/GotoNode.js @@ -0,0 +1,20 @@ +import React from 'react' +import {publish} from '../../../utils/pubsub.js'; + +export default function GotoNode(props) { + if((!props.treeAdapter.isArray(props.value) && !props.treeAdapter.isObject(props.value)) || props.treeAdapter.getRange(props.value) == undefined) { + return ( + <> + ); + } + + function goto() { + const range = props.treeAdapter.getRange(props.value) + + publish('SCROLL_TO_NODE', {value: props.value, range}) + } + + return ( + goto + ) +}