diff options
author | Omer Ben-Amram <[email protected]> | 2019-12-15 13:07:33 +0000 |
---|---|---|
committer | Omer Ben-Amram <[email protected]> | 2019-12-15 13:07:33 +0000 |
commit | 1d9b585c62dc92889380c9ae130d15ce7f9b08d4 (patch) | |
tree | 7c914d1fa72668dcc180b75eb24f20e534c1b223 /editors/code/src/notifications/publish_decorations.ts | |
parent | 6cbd8a4a4bbca8a7656df9f3ef849acebbf9ef9b (diff) |
make drive comparison case-insensitive.
Diffstat (limited to 'editors/code/src/notifications/publish_decorations.ts')
-rw-r--r-- | editors/code/src/notifications/publish_decorations.ts | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts index 00ffb7776..120eabbc6 100644 --- a/editors/code/src/notifications/publish_decorations.ts +++ b/editors/code/src/notifications/publish_decorations.ts | |||
@@ -10,10 +10,19 @@ export interface PublishDecorationsParams { | |||
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( |
13 | editor => editor.document.uri.toString() === params.uri, | 13 | editor => { |
14 | const unescapedUri = unescape(editor.document.uri.toString()); | ||
15 | // Unescaped URI should be something like: | ||
16 | // file:///c:/Workspace/ra-test/src/main.rs | ||
17 | // RA server might send it with the drive letter uppercased, so we force only the drive letter to lowercase. | ||
18 | const uriWithLowercasedDrive = params.uri.substr(0, 8) + params.uri[8].toLowerCase() + params.uri.substr(9); | ||
19 | return unescapedUri === uriWithLowercasedDrive | ||
20 | } | ||
14 | ); | 21 | ); |
22 | |||
15 | if (!Server.config.highlightingOn || !targetEditor) { | 23 | if (!Server.config.highlightingOn || !targetEditor) { |
16 | return; | 24 | return; |
17 | } | 25 | } |
26 | |||
18 | Server.highlighter.setHighlights(targetEditor, params.decorations); | 27 | Server.highlighter.setHighlights(targetEditor, params.decorations); |
19 | } | 28 | } |