diff options
author | Timo Freiberg <[email protected]> | 2020-04-20 17:02:36 +0100 |
---|---|---|
committer | Timo Freiberg <[email protected]> | 2020-04-21 22:04:44 +0100 |
commit | 74780a15f65916d08942eb53c43b8e8c0b62cb48 (patch) | |
tree | b34aefbe32e61d7c2630e74cde58060a850093e0 /editors/code | |
parent | ba8faf3efc7a3a373571f98569699bbe684779b3 (diff) |
Jump to sourceChanges in other files
Diffstat (limited to 'editors/code')
-rw-r--r-- | editors/code/src/source_change.ts | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/editors/code/src/source_change.ts b/editors/code/src/source_change.ts index 399a150c6..af8f1df51 100644 --- a/editors/code/src/source_change.ts +++ b/editors/code/src/source_change.ts | |||
@@ -37,11 +37,13 @@ export async function applySourceChange(ctx: Ctx, change: ra.SourceChange) { | |||
37 | toReveal.position, | 37 | toReveal.position, |
38 | ); | 38 | ); |
39 | const editor = vscode.window.activeTextEditor; | 39 | const editor = vscode.window.activeTextEditor; |
40 | if (!editor || editor.document.uri.toString() !== uri.toString()) { | 40 | if (!editor || !editor.selection.isEmpty) { |
41 | return; | 41 | return; |
42 | } | 42 | } |
43 | if (!editor.selection.isEmpty) { | 43 | |
44 | return; | 44 | if (editor.document.uri !== uri) { |
45 | const doc = await vscode.workspace.openTextDocument(uri); | ||
46 | await vscode.window.showTextDocument(doc); | ||
45 | } | 47 | } |
46 | editor.selection = new vscode.Selection(position, position); | 48 | editor.selection = new vscode.Selection(position, position); |
47 | editor.revealRange( | 49 | editor.revealRange( |