aboutsummaryrefslogtreecommitdiff
path: root/editors/code/src/notifications
diff options
context:
space:
mode:
authorbors[bot] <bors[bot]@users.noreply.github.com>2018-10-09 07:16:36 +0100
committerbors[bot] <bors[bot]@users.noreply.github.com>2018-10-09 07:16:36 +0100
commitc9798c0e6da53c132021f03ac7a50ccd8714b371 (patch)
tree0d6d49b2eb40ad161a72adbfbf9874b64540bf74 /editors/code/src/notifications
parentf4ad36e972989c3feed8671d6d6fca0aed37cd8f (diff)
parente26071d96e1ff56289213dbe78415f836de8a70e (diff)
Merge #104
104: Add vscode extension to CI r=aochagavia a=DJMcNab Note that this testing is only done on travis - we are only running formatting and linting, so feature parity on appveyor is not required. CC @aochagavia. Fixes? #100 Co-authored-by: Daniel McNab <[email protected]>
Diffstat (limited to 'editors/code/src/notifications')
-rw-r--r--editors/code/src/notifications/index.ts4
-rw-r--r--editors/code/src/notifications/publish_decorations.ts11
2 files changed, 6 insertions, 9 deletions
diff --git a/editors/code/src/notifications/index.ts b/editors/code/src/notifications/index.ts
index c56576865..74c4c3563 100644
--- a/editors/code/src/notifications/index.ts
+++ b/editors/code/src/notifications/index.ts
@@ -1,5 +1,3 @@
1import * as publishDecorations from './publish_decorations'; 1import * as publishDecorations from './publish_decorations';
2 2
3export { 3export { publishDecorations };
4 publishDecorations,
5};
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts
index d8790386b..3180019b7 100644
--- a/editors/code/src/notifications/publish_decorations.ts
+++ b/editors/code/src/notifications/publish_decorations.ts
@@ -10,11 +10,10 @@ 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 => editor.document.uri.toString() === params.uri
14 );
15 if (!Server.config.highlightingOn || !targetEditor) { return; }
16 Server.highlighter.setHighlights(
17 targetEditor,
18 params.decorations,
19 ); 14 );
15 if (!Server.config.highlightingOn || !targetEditor) {
16 return;
17 }
18 Server.highlighter.setHighlights(targetEditor, params.decorations);
20} 19}