Fix scrolling of jumpToOrigin
This commit is contained in:
parent
1891241d0a
commit
44159c63d1
|
|
@ -50,7 +50,7 @@ function jumpToOrigin(view: EditorView, type: { get: typeof getDefinition, capab
|
||||||
: plugin.fromPosition(loc.range.start, target.view.state.doc);
|
: plugin.fromPosition(loc.range.start, target.view.state.doc);
|
||||||
target.view.dispatch({
|
target.view.dispatch({
|
||||||
selection: {anchor: pos},
|
selection: {anchor: pos},
|
||||||
scrollIntoView: true,
|
effects: EditorView.scrollIntoView(pos, {y: "start"}),
|
||||||
userEvent: "select.definition",
|
userEvent: "select.definition",
|
||||||
});
|
});
|
||||||
setTimeout(() => target.focus(), 0);
|
setTimeout(() => target.focus(), 0);
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue