diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 1bb12306f..9dc513942 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,9 +25,7 @@ package workspace.plugins; import java.io.File; -import java.util.HashSet; import java.util.List; -import java.util.Set; import java.util.Vector; import com.fujitsu.vdmj.lex.Dialect; @@ -162,7 +160,6 @@ public RPCMessageList getJSONObligations(RPCRequest request, File file) messagehub.clearPluginMessages(this); List messages = new Vector(); - Set errFiles = new HashSet(); for (ProofObligation po: poGeneratedList) { @@ -228,14 +225,12 @@ else if (file.isDirectory()) } messages.add(new VDMWarning(9000, sb.toString(), po.location)); - errFiles.add(po.location.file); } if (po.countermessage != null) { json.put("message", "PO #" + po.number + ": " + po.countermessage); messages.add(new VDMWarning(9001, po.countermessage, po.location)); - errFiles.add(po.location.file); } poList.add(json); @@ -243,7 +238,7 @@ else if (file.isDirectory()) messagehub.addPluginMessages(this, messages); RPCMessageList result = new RPCMessageList(request, poList); - result.addAll(messagehub.getDiagnosticResponses(errFiles)); + result.addAll(messagehub.getDiagnosticResponses()); return result; } diff --git a/lsp/src/test/java/lsp/POGTest.java b/lsp/src/test/java/lsp/POGTest.java index fadc4fecf..66f854e24 100644 --- a/lsp/src/test/java/lsp/POGTest.java +++ b/lsp/src/test/java/lsp/POGTest.java @@ -65,7 +65,7 @@ public void testSL() throws Exception new JSONObject("uri", file.toURI().toString())); RPCMessageList response = handler.request(request); - assertEquals(1, response.size()); + assertEquals(2, response.size()); dump(response.get(0)); assertEquals("non-zero", response.get(0).getPath("result.[0].kind")); @@ -96,7 +96,7 @@ public void testPP() throws Exception new JSONObject("uri", testdir.toURI().toString())); RPCMessageList response = handler.request(request); - assertEquals(1, response.size()); + assertEquals(2, response.size()); dump(response.get(0)); assertEquals("non-zero", response.get(0).getPath("result.[0].kind")); @@ -127,7 +127,7 @@ public void testRT() throws Exception new JSONObject("uri", testdir.toURI().toString())); RPCMessageList response = handler.request(request); - assertEquals(1, response.size()); + assertEquals(2, response.size()); dump(response.get(0)); assertEquals("non-zero", response.get(0).getPath("result.[0].kind"));