From 18ff477d347c7c461bb3ae2b5e6eb32a61785365 Mon Sep 17 00:00:00 2001
From: Dave Holoway <adelphes@gmail.com>
Date: Sun, 7 Jun 2020 12:58:01 +0100
Subject: [PATCH] clear diagnostics when document is closed

---
 langserver/server.js | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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