diff options
author | Seivan Heidari <[email protected]> | 2019-12-23 14:35:31 +0000 |
---|---|---|
committer | Seivan Heidari <[email protected]> | 2019-12-23 14:35:31 +0000 |
commit | b21d9337d9200e2cfdc90b386591c72c302dc03e (patch) | |
tree | f81f5c08f821115cee26fa4d3ceaae88c7807fd5 /editors/code/src/commands/apply_source_change.ts | |
parent | 18a0937585b836ec5ed054b9ae48e0156ab6d9ef (diff) | |
parent | ce07a2daa9e53aa86a769f8641b14c2878444fbc (diff) |
Merge branch 'master' into feature/themes
Diffstat (limited to 'editors/code/src/commands/apply_source_change.ts')
-rw-r--r-- | editors/code/src/commands/apply_source_change.ts | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/editors/code/src/commands/apply_source_change.ts b/editors/code/src/commands/apply_source_change.ts index dcd074b8b..8167398b1 100644 --- a/editors/code/src/commands/apply_source_change.ts +++ b/editors/code/src/commands/apply_source_change.ts | |||
@@ -11,7 +11,7 @@ export interface SourceChange { | |||
11 | 11 | ||
12 | export async function handle(change: SourceChange) { | 12 | export async function handle(change: SourceChange) { |
13 | const wsEdit = Server.client.protocol2CodeConverter.asWorkspaceEdit( | 13 | const wsEdit = Server.client.protocol2CodeConverter.asWorkspaceEdit( |
14 | change.workspaceEdit | 14 | change.workspaceEdit, |
15 | ); | 15 | ); |
16 | let created; | 16 | let created; |
17 | let moved; | 17 | let moved; |
@@ -33,10 +33,10 @@ export async function handle(change: SourceChange) { | |||
33 | await vscode.window.showTextDocument(doc); | 33 | await vscode.window.showTextDocument(doc); |
34 | } else if (toReveal) { | 34 | } else if (toReveal) { |
35 | const uri = Server.client.protocol2CodeConverter.asUri( | 35 | const uri = Server.client.protocol2CodeConverter.asUri( |
36 | toReveal.textDocument.uri | 36 | toReveal.textDocument.uri, |
37 | ); | 37 | ); |
38 | const position = Server.client.protocol2CodeConverter.asPosition( | 38 | const position = Server.client.protocol2CodeConverter.asPosition( |
39 | toReveal.position | 39 | toReveal.position, |
40 | ); | 40 | ); |
41 | const editor = vscode.window.activeTextEditor; | 41 | const editor = vscode.window.activeTextEditor; |
42 | if (!editor || editor.document.uri.toString() !== uri.toString()) { | 42 | if (!editor || editor.document.uri.toString() !== uri.toString()) { |
@@ -48,7 +48,7 @@ export async function handle(change: SourceChange) { | |||
48 | editor.selection = new vscode.Selection(position, position); | 48 | editor.selection = new vscode.Selection(position, position); |
49 | editor.revealRange( | 49 | editor.revealRange( |
50 | new vscode.Range(position, position), | 50 | new vscode.Range(position, position), |
51 | vscode.TextEditorRevealType.Default | 51 | vscode.TextEditorRevealType.Default, |
52 | ); | 52 | ); |
53 | } | 53 | } |
54 | } | 54 | } |