clear diagnostics when document is closed

This commit is contained in:
Dave Holoway
2020-06-07 12:58:01 +01:00
parent de846fef12
commit 18ff477d34

View File

@@ -228,9 +228,10 @@ function getDocumentSettings(resource) {
// Only keep settings for open documents // Only keep settings for open documents
documents.onDidClose((e) => { documents.onDidClose((e) => {
connection.console.log('doc closed'); connection.console.log(`doc closed ${e.document.uri}`);
parsed = null; parsed = null;
documentSettings.delete(e.document.uri); documentSettings.delete(e.document.uri);
connection.sendDiagnostics({ uri: e.document.uri, diagnostics: [] });
}); });
// The content of a text document has changed. This event is emitted // The content of a text document has changed. This event is emitted