From 29707d061467caf4f5ee16262dbb027f0679c7e8 Mon Sep 17 00:00:00 2001 From: BoykoAlex Date: Thu, 2 Aug 2018 18:40:50 -0400 Subject: [PATCH] Fix flickering of boot hints for VSCode client --- .../commons-vscode/src/highlight-service.ts | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/vscode-extensions/commons-vscode/src/highlight-service.ts b/vscode-extensions/commons-vscode/src/highlight-service.ts index e55545b4c..974653dcf 100644 --- a/vscode-extensions/commons-vscode/src/highlight-service.ts +++ b/vscode-extensions/commons-vscode/src/highlight-service.ts @@ -1,4 +1,4 @@ -import {TextDocumentIdentifier, Position, Range} from 'vscode-languageclient' +import {VersionedTextDocumentIdentifier, Position, Range} from 'vscode-languageclient' import * as VSCode from 'vscode'; import * as path from "path"; @@ -11,7 +11,7 @@ function toPosition(p : Position) : VSCode.Position { } export interface HighlightParams { - doc: TextDocumentIdentifier + doc: VersionedTextDocumentIdentifier ranges: Range[] } @@ -42,16 +42,17 @@ export class HighlightService { handle(params : HighlightParams) : void { this.highlights.set(params.doc.uri, params.ranges); - this.refresh(params.doc.uri); + this.refresh(params.doc); } - refresh(uri : String) { + refresh(docId: VersionedTextDocumentIdentifier) { let editors = VSCode.window.visibleTextEditors; for (let editor of editors) { - let activeUri = editor.document.uri.toString(); - if (uri===activeUri) { + const activeUri = editor.document.uri.toString(); + const activeVersion = editor.document.version; + if (docId.uri === activeUri && docId.version === activeVersion) { //We only update highlights in the active editor for now - let highlights : Range[] = this.highlights.get(uri) || []; + let highlights : Range[] = this.highlights.get(docId.uri) || []; let decorations = highlights.map(hl => toDecoration(hl)); editor.setDecorations(this.DECORATION, decorations); editor.setDecorations(this.DECORATION, decorations);