|
@@ -122,12 +122,13 @@ const dispatchSelectionAndScroll = (
|
|
|
view: EditorView,
|
|
view: EditorView,
|
|
|
selection: SelectionRange
|
|
selection: SelectionRange
|
|
|
) => {
|
|
) => {
|
|
|
- view.dispatch({
|
|
|
|
|
- selection,
|
|
|
|
|
- effects: EditorView.scrollIntoView(selection, { y: 'center' }),
|
|
|
|
|
|
|
+ window.setTimeout(() => {
|
|
|
|
|
+ view.dispatch({
|
|
|
|
|
+ selection,
|
|
|
|
|
+ effects: EditorView.scrollIntoView(selection, { y: 'center' }),
|
|
|
|
|
+ })
|
|
|
|
|
+ view.focus()
|
|
|
})
|
|
})
|
|
|
-
|
|
|
|
|
- view.focus()
|
|
|
|
|
}
|
|
}
|
|
|
|
|
|
|
|
export const setCursorLineAndScroll = (
|
|
export const setCursorLineAndScroll = (
|