Skip to content

Commit 90dcdfa

Browse files
authored
Merge pull request #108 from lovettchris/clovett/fix71
fix: reveal file location should move the keyboard focus to the text editor
2 parents 9eeb84a + f0c3806 commit 90dcdfa

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

vscode-lean4/src/infoview.ts

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -379,6 +379,8 @@ export class InfoProvider implements Disposable {
379379
if (selection !== undefined) {
380380
editor.revealRange(selection, TextEditorRevealType.InCenterIfOutsideViewport);
381381
editor.selection = new Selection(selection.start, selection.end);
382+
// ensure the text document has the keyboard focus.
383+
void window.showTextDocument(editor.document, { viewColumn: editor.viewColumn, preserveFocus: false });
382384
}
383385
}
384386

0 commit comments

Comments
 (0)