Reveal the newly added source change in the editor.

2019-01-14 17:24:49 -05:00 · 2019-01-14 17:24:49 -05:00 · cd21f0eade
commit cd21f0eade
parent e8e82ce032
1 changed files with 1 additions and 0 deletions
--- a/editors/code/src/commands/apply_source_change.ts
+++ b/editors/code/src/commands/apply_source_change.ts
@ -46,5 +46,6 @@ export async function handle(change: SourceChange) {
            return;
        }
        editor.selection = new vscode.Selection(position, position);
+        editor.revealRange(new vscode.Range(position, position), vscode.TextEditorRevealType.Default);
    }
 }