Skip to content

Commit

Permalink
Fix LSP tests and PO error messages
Browse files Browse the repository at this point in the history
  • Loading branch information
nickbattle committed Oct 30, 2023
1 parent c912737 commit 4d0ee00
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 9 deletions.
7 changes: 1 addition & 6 deletions lsp/src/main/java/workspace/plugins/POPlugin.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -162,7 +160,6 @@ public RPCMessageList getJSONObligations(RPCRequest request, File file)

messagehub.clearPluginMessages(this);
List<VDMMessage> messages = new Vector<VDMMessage>();
Set<File> errFiles = new HashSet<File>();

for (ProofObligation po: poGeneratedList)
{
Expand Down Expand Up @@ -228,22 +225,20 @@ 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);
}

messagehub.addPluginMessages(this, messages);
RPCMessageList result = new RPCMessageList(request, poList);
result.addAll(messagehub.getDiagnosticResponses(errFiles));
result.addAll(messagehub.getDiagnosticResponses());

return result;
}
Expand Down
6 changes: 3 additions & 3 deletions lsp/src/test/java/lsp/POGTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -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"));
Expand Down Expand Up @@ -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"));
Expand Down Expand Up @@ -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"));
Expand Down

0 comments on commit 4d0ee00

Please sign in to comment.