Deal with delete/rename of external files with errs/warns

nickbattle · Nov 7, 2023 · 4f5ebfe · 4f5ebfe
1 parent 769060a
commit 4f5ebfe
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/lsp/src/main/java/workspace/LSPWorkspaceManager.java b/lsp/src/main/java/workspace/LSPWorkspaceManager.java
@@ -1130,6 +1130,11 @@ public RPCMessageList afterChangeWatchedFiles(RPCRequest request, int actionCode
 			{
 				for (File file: deleted)
 				{
+					if (isExternalFile(file))
+					{
+						file = getExtractedName(file);	// Messages reported against extract
+					}
+
 					JSONObject params = new JSONObject("uri", file.toURI().toString(), "diagnostics", new JSONArray());
 					results.add(RPCRequest.notification("textDocument/publishDiagnostics", params));
 				}