diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2019-12-30 22:24:39 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2019-12-30 22:24:39 +0000 |
commit | e6a1ccc1f49488af31ff7429ff977768d3d32485 (patch) | |
tree | 0e6c920b9bb1955de444dc360072b2256060d89b /editors/code/src/notifications | |
parent | c3d74744cdae29aa6a6bfa0cd7ab64b8b251e287 (diff) | |
parent | 233f1dd2a850a7c8c6947c88c1ce06f7a945befd (diff) |
Merge #2695
2695: Privatize highlighting r=matklad a=matklad
Co-authored-by: Aleksey Kladov <[email protected]>
Diffstat (limited to 'editors/code/src/notifications')
-rw-r--r-- | editors/code/src/notifications/index.ts | 3 | ||||
-rw-r--r-- | editors/code/src/notifications/publish_decorations.ts | 24 |
2 files changed, 0 insertions, 27 deletions
diff --git a/editors/code/src/notifications/index.ts b/editors/code/src/notifications/index.ts deleted file mode 100644 index 74c4c3563..000000000 --- a/editors/code/src/notifications/index.ts +++ /dev/null | |||
@@ -1,3 +0,0 @@ | |||
1 | import * as publishDecorations from './publish_decorations'; | ||
2 | |||
3 | export { publishDecorations }; | ||
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts deleted file mode 100644 index f23e286ad..000000000 --- a/editors/code/src/notifications/publish_decorations.ts +++ /dev/null | |||
@@ -1,24 +0,0 @@ | |||
1 | import * as vscode from 'vscode'; | ||
2 | |||
3 | import { Decoration } from '../highlighting'; | ||
4 | import { Server } from '../server'; | ||
5 | |||
6 | export interface PublishDecorationsParams { | ||
7 | uri: string; | ||
8 | decorations: Decoration[]; | ||
9 | } | ||
10 | |||
11 | export function handle(params: PublishDecorationsParams) { | ||
12 | const targetEditor = vscode.window.visibleTextEditors.find(editor => { | ||
13 | const unescapedUri = unescape(editor.document.uri.toString()); | ||
14 | // Unescaped URI looks like: | ||
15 | // file:///c:/Workspace/ra-test/src/main.rs | ||
16 | return unescapedUri === params.uri; | ||
17 | }); | ||
18 | |||
19 | if (!Server.config.highlightingOn || !targetEditor) { | ||
20 | return; | ||
21 | } | ||
22 | |||
23 | Server.highlighter.setHighlights(targetEditor, params.decorations); | ||
24 | } | ||