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..1bb12306f 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -25,7 +25,6 @@ package workspace.plugins; import java.io.File; -import java.io.IOException; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -41,7 +40,6 @@ import json.JSONArray; import json.JSONObject; -import lsp.LSPServer; import lsp.Utils; import rpc.RPCMessageList; import rpc.RPCRequest; @@ -157,10 +155,10 @@ 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(); @@ -240,24 +238,13 @@ else if (file.isDirectory()) 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(errFiles)); - for (JSONObject err: errs) - { - try - { - LSPServer.getInstance().writeMessage(err); - } - catch (IOException e) - { - Diag.error(e); - } - } - - return results; // Just POG display results + return result; } }