diff --git a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java index c3f092108..cb121980d 100644 --- a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java +++ b/lsp/src/main/java/workspace/LSPXWorkspaceManager.java @@ -202,8 +202,7 @@ public RPCMessageList pogGenerate(RPCRequest request, File file) } POPlugin po = registry.getPlugin("PO"); - JSONArray results = po.getObligations(file); - return new RPCMessageList(request, results); + return po.getJSONObligations(request, file); } catch (Exception e) { diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index b5ed49862..9dc513942 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,10 +25,7 @@ package workspace.plugins; import java.io.File; -import java.io.IOException; -import java.util.HashSet; import java.util.List; -import java.util.Set; import java.util.Vector; import com.fujitsu.vdmj.lex.Dialect; @@ -41,7 +38,6 @@ import json.JSONArray; import json.JSONObject; -import lsp.LSPServer; import lsp.Utils; import rpc.RPCMessageList; import rpc.RPCRequest; @@ -157,14 +153,13 @@ protected JSONArray splitPO(String value) return array; } - public JSONArray getObligations(File file) + public RPCMessageList getJSONObligations(RPCRequest request, File file) { ProofObligationList poGeneratedList = getProofObligations(); - JSONArray results = new JSONArray(); + JSONArray poList = new JSONArray(); messagehub.clearPluginMessages(this); List messages = new Vector(); - Set errFiles = new HashSet(); for (ProofObligation po: poGeneratedList) { @@ -230,34 +225,21 @@ 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); } - results.add(json); + poList.add(json); } messagehub.addPluginMessages(this, messages); - RPCMessageList errs = messagehub.getDiagnosticResponses(errFiles); + RPCMessageList result = new RPCMessageList(request, poList); + result.addAll(messagehub.getDiagnosticResponses()); - for (JSONObject err: errs) - { - try - { - LSPServer.getInstance().writeMessage(err); - } - catch (IOException e) - { - Diag.error(e); - } - } - - return results; // Just POG display results + 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"));