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/notifications | |
parent | 18a0937585b836ec5ed054b9ae48e0156ab6d9ef (diff) | |
parent | ce07a2daa9e53aa86a769f8641b14c2878444fbc (diff) |
Merge branch 'master' into feature/themes
Diffstat (limited to 'editors/code/src/notifications')
-rw-r--r-- | editors/code/src/notifications/publish_decorations.ts | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts index 3180019b7..f23e286ad 100644 --- a/editors/code/src/notifications/publish_decorations.ts +++ b/editors/code/src/notifications/publish_decorations.ts | |||
@@ -9,11 +9,16 @@ export interface PublishDecorationsParams { | |||
9 | } | 9 | } |
10 | 10 | ||
11 | export function handle(params: PublishDecorationsParams) { | 11 | export function handle(params: PublishDecorationsParams) { |
12 | const targetEditor = vscode.window.visibleTextEditors.find( | 12 | const targetEditor = vscode.window.visibleTextEditors.find(editor => { |
13 | editor => editor.document.uri.toString() === params.uri | 13 | const unescapedUri = unescape(editor.document.uri.toString()); |
14 | ); | 14 | // Unescaped URI looks like: |
15 | // file:///c:/Workspace/ra-test/src/main.rs | ||
16 | return unescapedUri === params.uri; | ||
17 | }); | ||
18 | |||
15 | if (!Server.config.highlightingOn || !targetEditor) { | 19 | if (!Server.config.highlightingOn || !targetEditor) { |
16 | return; | 20 | return; |
17 | } | 21 | } |
22 | |||
18 | Server.highlighter.setHighlights(targetEditor, params.decorations); | 23 | Server.highlighter.setHighlights(targetEditor, params.decorations); |
19 | } | 24 | } |