aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorOmer Ben-Amram <[email protected]>2019-12-15 13:07:33 +0000
committerOmer Ben-Amram <[email protected]>2019-12-15 13:07:33 +0000
commit1d9b585c62dc92889380c9ae130d15ce7f9b08d4 (patch)
tree7c914d1fa72668dcc180b75eb24f20e534c1b223
parent6cbd8a4a4bbca8a7656df9f3ef849acebbf9ef9b (diff)
make drive comparison case-insensitive.
-rw-r--r--editors/code/src/notifications/publish_decorations.ts11
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
11export function handle(params: PublishDecorationsParams) { 11export 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}