diff --git a/examples/lspplugin/src/main/resources/META-INF/plugin.json b/examples/lspplugin/src/main/resources/META-INF/plugin.json new file mode 100644 index 000000000..31b597915 --- /dev/null +++ b/examples/lspplugin/src/main/resources/META-INF/plugin.json @@ -0,0 +1,6 @@ +{ + "name": "ExamplePlugin", + "description": "Example LSP plugin", + "dialects": [ "vdmsl", "vdmpp", "vdmrt" ], + "precision": "standard" +} diff --git a/examples/v2c/src/test/java/plugins/LSPTest.java b/examples/v2c/src/test/java/plugins/LSPTest.java index 8f5ce4284..1552081ef 100644 --- a/examples/v2c/src/test/java/plugins/LSPTest.java +++ b/examples/v2c/src/test/java/plugins/LSPTest.java @@ -36,16 +36,14 @@ import json.JSONWriter; import rpc.RPCMessageList; import rpc.RPCRequest; -import workspace.DAPWorkspaceManager; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.DAPPlugin; +import workspace.plugins.LSPPlugin; abstract public class LSPTest { - protected LSPWorkspaceManager lspManager = null; - protected LSPXWorkspaceManager lspxManager = null; - protected DAPWorkspaceManager dapManager = null; + protected LSPPlugin lspManager = null; + protected DAPPlugin dapManager = null; static { @@ -55,12 +53,10 @@ abstract public class LSPTest protected void setupWorkspace(Dialect dialect) throws IOException { Settings.dialect = dialect; - LSPWorkspaceManager.reset(); - LSPXWorkspaceManager.reset(); - DAPWorkspaceManager.reset(); - lspManager = LSPWorkspaceManager.getInstance(); - lspxManager = LSPXWorkspaceManager.getInstance(); - dapManager = DAPWorkspaceManager.getInstance(); + LSPPlugin.reset(); + DAPPlugin.reset(); + lspManager = LSPPlugin.getInstance(); + dapManager = DAPPlugin.getInstance(); } protected RPCMessageList initialize(File root, JSONObject capabilities) throws Exception diff --git a/lsp/documentation/DesignSpec.odt b/lsp/documentation/DesignSpec.odt index 96a340093..8587a461a 100644 Binary files a/lsp/documentation/DesignSpec.odt and b/lsp/documentation/DesignSpec.odt differ diff --git a/lsp/documentation/DesignSpec.pdf b/lsp/documentation/DesignSpec.pdf index 9ba8143d5..dfc81a187 100644 Binary files a/lsp/documentation/DesignSpec.pdf and b/lsp/documentation/DesignSpec.pdf differ diff --git a/lsp/documentation/PluginWritersGuide.odt b/lsp/documentation/PluginWritersGuide.odt index 65520c9b3..a0bebaae4 100644 Binary files a/lsp/documentation/PluginWritersGuide.odt and b/lsp/documentation/PluginWritersGuide.odt differ diff --git a/lsp/documentation/PluginWritersGuide.pdf b/lsp/documentation/PluginWritersGuide.pdf index d32e2c020..4674702a3 100644 Binary files a/lsp/documentation/PluginWritersGuide.pdf and b/lsp/documentation/PluginWritersGuide.pdf differ diff --git a/lsp/src/main/java/dap/AsyncExecutor.java b/lsp/src/main/java/dap/AsyncExecutor.java index 4d51014df..a46c00f29 100644 --- a/lsp/src/main/java/dap/AsyncExecutor.java +++ b/lsp/src/main/java/dap/AsyncExecutor.java @@ -30,13 +30,13 @@ import lsp.CancellableThread; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public abstract class AsyncExecutor extends CancellableThread { protected final DAPServer server = DAPServer.getInstance(); - protected final DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + protected final DAPPlugin manager = DAPPlugin.getInstance(); protected final DAPRequest request; public AsyncExecutor(String id, DAPRequest request) diff --git a/lsp/src/main/java/dap/DAPServer.java b/lsp/src/main/java/dap/DAPServer.java index e48fcf37e..a882ed983 100644 --- a/lsp/src/main/java/dap/DAPServer.java +++ b/lsp/src/main/java/dap/DAPServer.java @@ -45,8 +45,8 @@ import dap.handlers.ThreadsHandler; import json.JSONObject; import json.JSONServer; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class DAPServer extends JSONServer { @@ -61,7 +61,7 @@ public DAPServer(Dialect dialect, Socket socket) throws IOException INSTANCE = this; this.dispatcher = getDispatcher(); - DAPWorkspaceManager.getInstance(); // Just set up + DAPPlugin.getInstance(); // Just set up } public static DAPServer getInstance() diff --git a/lsp/src/main/java/dap/UnknownHandler.java b/lsp/src/main/java/dap/UnknownHandler.java index 6a44e766e..498c5548a 100644 --- a/lsp/src/main/java/dap/UnknownHandler.java +++ b/lsp/src/main/java/dap/UnknownHandler.java @@ -27,7 +27,7 @@ import java.io.IOException; -import workspace.DAPXWorkspaceManager; +import workspace.plugins.DAPPlugin; public class UnknownHandler extends DAPHandler { @@ -39,7 +39,7 @@ public UnknownHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPXWorkspaceManager manager = DAPXWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); return manager.unhandledCommand(request); } } diff --git a/lsp/src/main/java/dap/handlers/DebuggingHandler.java b/lsp/src/main/java/dap/handlers/DebuggingHandler.java index fd103c9f2..ea61a8da1 100644 --- a/lsp/src/main/java/dap/handlers/DebuggingHandler.java +++ b/lsp/src/main/java/dap/handlers/DebuggingHandler.java @@ -30,8 +30,8 @@ import dap.DAPMessageList; import dap.DAPRequest; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class DebuggingHandler extends DAPHandler { @@ -43,7 +43,7 @@ public DebuggingHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) diff --git a/lsp/src/main/java/dap/handlers/DisconnectHandler.java b/lsp/src/main/java/dap/handlers/DisconnectHandler.java index 6da6a59c9..123b4717d 100644 --- a/lsp/src/main/java/dap/handlers/DisconnectHandler.java +++ b/lsp/src/main/java/dap/handlers/DisconnectHandler.java @@ -34,7 +34,7 @@ import lsp.CancellableThread; import lsp.Utils; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class DisconnectHandler extends DAPHandler { @@ -46,7 +46,7 @@ public DisconnectHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null) diff --git a/lsp/src/main/java/dap/handlers/EvaluateHandler.java b/lsp/src/main/java/dap/handlers/EvaluateHandler.java index e8f00305c..b90c689f7 100644 --- a/lsp/src/main/java/dap/handlers/EvaluateHandler.java +++ b/lsp/src/main/java/dap/handlers/EvaluateHandler.java @@ -31,7 +31,7 @@ import dap.DAPRequest; import json.JSONObject; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class EvaluateHandler extends DAPHandler { @@ -43,7 +43,7 @@ public EvaluateHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) diff --git a/lsp/src/main/java/dap/handlers/InitializeHandler.java b/lsp/src/main/java/dap/handlers/InitializeHandler.java index 5eeb4a1ec..a4557ed72 100644 --- a/lsp/src/main/java/dap/handlers/InitializeHandler.java +++ b/lsp/src/main/java/dap/handlers/InitializeHandler.java @@ -30,8 +30,8 @@ import dap.DAPMessageList; import dap.DAPRequest; import json.JSONObject; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class InitializeHandler extends DAPHandler { @@ -60,7 +60,7 @@ private DAPMessageList initialize(DAPRequest request) try { JSONObject arguments = request.get("arguments"); - return DAPWorkspaceManager.getInstance().dapInitialize(request, arguments); + return DAPPlugin.getInstance().dapInitialize(request, arguments); } catch (Exception e) { @@ -73,7 +73,7 @@ private DAPMessageList configurationDone(DAPRequest request) { try { - return DAPWorkspaceManager.getInstance().dapConfigurationDone(request); + return DAPPlugin.getInstance().dapConfigurationDone(request); } catch (Exception e) { diff --git a/lsp/src/main/java/dap/handlers/LaunchHandler.java b/lsp/src/main/java/dap/handlers/LaunchHandler.java index e3720384c..79968629b 100644 --- a/lsp/src/main/java/dap/handlers/LaunchHandler.java +++ b/lsp/src/main/java/dap/handlers/LaunchHandler.java @@ -29,7 +29,7 @@ import dap.DAPMessageList; import dap.DAPRequest; import json.JSONObject; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class LaunchHandler extends DAPHandler { @@ -50,7 +50,7 @@ public DAPMessageList run(DAPRequest request) throws IOException String remoteControl = arguments.get("remoteControl"); String logging = arguments.get("logging"); - return DAPWorkspaceManager.getInstance().dapLaunch( + return DAPPlugin.getInstance().dapLaunch( request, noDebug, defaultName, command, remoteControl, logging); } catch (Exception e) diff --git a/lsp/src/main/java/dap/handlers/PauseHandler.java b/lsp/src/main/java/dap/handlers/PauseHandler.java index 12a5e8ee5..d53ee91cd 100644 --- a/lsp/src/main/java/dap/handlers/PauseHandler.java +++ b/lsp/src/main/java/dap/handlers/PauseHandler.java @@ -31,8 +31,8 @@ import dap.DAPMessageList; import dap.DAPRequest; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class PauseHandler extends DAPHandler { @@ -44,7 +44,7 @@ public PauseHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null) diff --git a/lsp/src/main/java/dap/handlers/SetBreakpointsHandler.java b/lsp/src/main/java/dap/handlers/SetBreakpointsHandler.java index e6a330c77..0f7beace4 100644 --- a/lsp/src/main/java/dap/handlers/SetBreakpointsHandler.java +++ b/lsp/src/main/java/dap/handlers/SetBreakpointsHandler.java @@ -34,7 +34,7 @@ import json.JSONObject; import lsp.Utils; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class SetBreakpointsHandler extends DAPHandler { @@ -67,7 +67,7 @@ private DAPMessageList setBreakpoints(DAPRequest request) throws IOException { try { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) @@ -82,7 +82,7 @@ private DAPMessageList setBreakpoints(DAPRequest request) throws IOException File file = Utils.pathToFile(source.get("path")); JSONArray breakpoints = arguments.get("breakpoints"); - return DAPWorkspaceManager.getInstance().dapSetBreakpoints(request, file, breakpoints); + return DAPPlugin.getInstance().dapSetBreakpoints(request, file, breakpoints); } } catch (Exception e) @@ -95,7 +95,7 @@ private DAPMessageList setFunctionBreakpoints(DAPRequest request) throws IOExcep { try { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) @@ -108,7 +108,7 @@ private DAPMessageList setFunctionBreakpoints(DAPRequest request) throws IOExcep JSONObject arguments = request.get("arguments"); JSONArray breakpoints = arguments.get("breakpoints"); - return DAPWorkspaceManager.getInstance().dapSetFunctionBreakpoints(request, breakpoints); + return DAPPlugin.getInstance().dapSetFunctionBreakpoints(request, breakpoints); } } catch (Exception e) @@ -121,7 +121,7 @@ private DAPMessageList setExceptionBreakpoints(DAPRequest request) throws IOExce { try { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) diff --git a/lsp/src/main/java/dap/handlers/StackTraceHandler.java b/lsp/src/main/java/dap/handlers/StackTraceHandler.java index 26d910072..1dc192b77 100644 --- a/lsp/src/main/java/dap/handlers/StackTraceHandler.java +++ b/lsp/src/main/java/dap/handlers/StackTraceHandler.java @@ -32,7 +32,7 @@ import json.JSONArray; import json.JSONObject; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class StackTraceHandler extends DAPHandler { @@ -44,7 +44,7 @@ public StackTraceHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) diff --git a/lsp/src/main/java/dap/handlers/TerminateHandler.java b/lsp/src/main/java/dap/handlers/TerminateHandler.java index 9aaf6ae72..fdab03cc2 100644 --- a/lsp/src/main/java/dap/handlers/TerminateHandler.java +++ b/lsp/src/main/java/dap/handlers/TerminateHandler.java @@ -32,7 +32,7 @@ import json.JSONObject; import lsp.CancellableThread; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class TerminateHandler extends DAPHandler { @@ -44,7 +44,7 @@ public TerminateHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null) diff --git a/lsp/src/main/java/dap/handlers/ThreadsHandler.java b/lsp/src/main/java/dap/handlers/ThreadsHandler.java index 6ce5607b7..ff1afa616 100644 --- a/lsp/src/main/java/dap/handlers/ThreadsHandler.java +++ b/lsp/src/main/java/dap/handlers/ThreadsHandler.java @@ -35,8 +35,8 @@ import json.JSONArray; import json.JSONObject; import vdmj.DAPDebugReader; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class ThreadsHandler extends DAPHandler { @@ -48,7 +48,7 @@ public ThreadsHandler() @Override public DAPMessageList run(DAPRequest request) throws IOException { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); DAPDebugReader debugReader = manager.getDebugReader(); if (debugReader != null && debugReader.isListening()) diff --git a/lsp/src/main/java/lsp/InitializeHandler.java b/lsp/src/main/java/lsp/InitializeHandler.java index 0051f1624..b0bde6de4 100644 --- a/lsp/src/main/java/lsp/InitializeHandler.java +++ b/lsp/src/main/java/lsp/InitializeHandler.java @@ -27,7 +27,8 @@ import rpc.RPCRequest; import rpc.RPCResponse; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; + import java.io.File; import java.net.URISyntaxException; @@ -72,8 +73,9 @@ private RPCMessageList initialize(RPCRequest request) rootUri = new File(".").getCanonicalFile(); // Some editors don't set the root? Diag.config("Assuming rootUri = %s", rootUri); } - - return LSPWorkspaceManager.getInstance().lspInitialize(request, clientInfo, rootUri, clientCapabilities); + + LSPPlugin lsp = LSPPlugin.getInstance(); + return lsp.lspInitialize(request, clientInfo, rootUri, clientCapabilities); } catch (URISyntaxException e) { @@ -90,7 +92,8 @@ private RPCMessageList initialize(RPCRequest request) private RPCMessageList initialized(RPCRequest request) { LSPServer.getInstance().setInitialized(true); - return LSPWorkspaceManager.getInstance().lspInitialized(request); + LSPPlugin lsp = LSPPlugin.getInstance(); + return lsp.lspInitialized(request); } @Override diff --git a/lsp/src/main/java/lsp/LSPHandler.java b/lsp/src/main/java/lsp/LSPHandler.java index d6598393f..2f8728399 100644 --- a/lsp/src/main/java/lsp/LSPHandler.java +++ b/lsp/src/main/java/lsp/LSPHandler.java @@ -29,11 +29,15 @@ import rpc.RPCRequest; import rpc.RPCResponse; import workspace.Diag; +import workspace.PluginRegistry; abstract public class LSPHandler implements RPCHandler { + protected final PluginRegistry registry; + public LSPHandler() { + registry = PluginRegistry.getInstance(); } @Override diff --git a/lsp/src/main/java/lsp/LSPInitializeResponse.java b/lsp/src/main/java/lsp/LSPInitializeResponse.java index 1edf6b314..2194a4a36 100644 --- a/lsp/src/main/java/lsp/LSPInitializeResponse.java +++ b/lsp/src/main/java/lsp/LSPInitializeResponse.java @@ -27,8 +27,8 @@ import dap.DAPServerSocket; import json.JSONArray; import json.JSONObject; -import workspace.LSPWorkspaceManager; import workspace.PluginRegistry; +import workspace.plugins.LSPPlugin; public class LSPInitializeResponse extends JSONObject { @@ -45,7 +45,7 @@ public LSPInitializeResponse() private JSONObject getServerCapabilities() { JSONObject cap = new JSONObject(); - LSPWorkspaceManager manager = LSPWorkspaceManager.getInstance(); + LSPPlugin manager = LSPPlugin.getInstance(); cap.put("definitionProvider", true); // Go to definition for F12 diff --git a/lsp/src/main/java/lsp/LSPServer.java b/lsp/src/main/java/lsp/LSPServer.java index 8e4632782..a6b52af7f 100644 --- a/lsp/src/main/java/lsp/LSPServer.java +++ b/lsp/src/main/java/lsp/LSPServer.java @@ -36,20 +36,6 @@ import json.JSONObject; import json.JSONServer; -import lsp.lspx.CTHandler; -import lsp.lspx.POGHandler; -import lsp.lspx.TranslateHandler; -import lsp.textdocument.CodeLensHandler; -import lsp.textdocument.CompletionHandler; -import lsp.textdocument.DefinitionHandler; -import lsp.textdocument.DidChangeHandler; -import lsp.textdocument.DidCloseHandler; -import lsp.textdocument.DidOpenHandler; -import lsp.textdocument.DidSaveHandler; -import lsp.textdocument.DocumentSymbolHandler; -import lsp.textdocument.ReferencesHandler; -import lsp.textdocument.TypeHierarchyHandler; -import lsp.workspace.DidChangeWSHandler; import rpc.RPCDispatcher; import rpc.RPCHandler; import rpc.RPCMessageList; @@ -57,6 +43,7 @@ import rpc.RPCResponse; import vdmj.DAPDebugLink; import workspace.Diag; +import workspace.plugins.LSPPlugin; public class LSPServer extends JSONServer implements VDMJMain { @@ -76,7 +63,7 @@ public LSPServer(Dialect dialect, InputStream inStream, OutputStream outStream) super("LSP", inStream, outStream); INSTANCE = this; - this.dispatcher = getDispatcher(); + this.dispatcher = RPCDispatcher.getInstance(); this.responseHandlers = new HashMap(); // Identify this class as the debug link - See DebugLink @@ -87,6 +74,8 @@ public LSPServer(Dialect dialect, InputStream inStream, OutputStream outStream) Settings.dialect = dialect; Settings.strict = Boolean.getBoolean("vdmj.strict"); Settings.verbose = Boolean.getBoolean("vdmj.verbose"); + + LSPPlugin.getInstance(); // Creates all plugins } public static LSPServer getInstance() @@ -94,38 +83,6 @@ public static LSPServer getInstance() return INSTANCE; } - private RPCDispatcher getDispatcher() throws IOException - { - RPCDispatcher dispatcher = RPCDispatcher.getInstance(); - - dispatcher.register(new InitializeHandler(), "initialize", "initialized", "client/registerCapability"); - dispatcher.register(new ShutdownHandler(), "shutdown"); - dispatcher.register(new ExitHandler(), "exit"); - dispatcher.register(new CancelHandler(), "$/cancelRequest"); - dispatcher.register(new SetTraceNotificationHandler(), "$/setTraceNotification", "$/setTrace"); - - dispatcher.register(new DidOpenHandler(), "textDocument/didOpen"); - dispatcher.register(new DidCloseHandler(), "textDocument/didClose"); - dispatcher.register(new DidChangeHandler(), "textDocument/didChange"); - dispatcher.register(new DidSaveHandler(), "textDocument/didSave"); - dispatcher.register(new DefinitionHandler(), "textDocument/definition"); - dispatcher.register(new DocumentSymbolHandler(), "textDocument/documentSymbol"); - dispatcher.register(new CompletionHandler(), "textDocument/completion"); - dispatcher.register(new CodeLensHandler(), "textDocument/codeLens", "codeLens/resolve"); - dispatcher.register(new ReferencesHandler(), "textDocument/references"); - dispatcher.register(new TypeHierarchyHandler(), "textDocument/prepareTypeHierarchy", "typeHierarchy/supertypes", "typeHierarchy/subtypes"); - - dispatcher.register(new DidChangeWSHandler(), "workspace/didChangeWatchedFiles"); - - dispatcher.register(new POGHandler(), "slsp/POG/generate"); - dispatcher.register(new CTHandler(), "slsp/CT/traces", "slsp/CT/generate", "slsp/CT/execute"); - dispatcher.register(new TranslateHandler(), "slsp/TR/translate"); - - dispatcher.register(new UnknownHandler()); // Called for unknown methods - - return dispatcher; - } - public void run() throws IOException { boolean running = true; diff --git a/lsp/src/main/java/lsp/ShutdownHandler.java b/lsp/src/main/java/lsp/ShutdownHandler.java index ffb7b4649..ad1fc76e0 100644 --- a/lsp/src/main/java/lsp/ShutdownHandler.java +++ b/lsp/src/main/java/lsp/ShutdownHandler.java @@ -25,7 +25,7 @@ package lsp; import rpc.RPCRequest; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; import rpc.RPCMessageList; public class ShutdownHandler extends LSPHandler @@ -38,6 +38,6 @@ public ShutdownHandler() @Override public RPCMessageList request(RPCRequest request) { - return LSPWorkspaceManager.getInstance().lspShutdown(request); + return LSPPlugin.getInstance().lspShutdown(request); } } diff --git a/lsp/src/main/java/lsp/UnknownHandler.java b/lsp/src/main/java/lsp/UnknownHandler.java index f62976d60..0aa3b623f 100644 --- a/lsp/src/main/java/lsp/UnknownHandler.java +++ b/lsp/src/main/java/lsp/UnknownHandler.java @@ -25,7 +25,7 @@ package lsp; import rpc.RPCRequest; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.LSPPlugin; import rpc.RPCMessageList; public class UnknownHandler extends LSPHandler @@ -38,7 +38,7 @@ public UnknownHandler() @Override public RPCMessageList request(RPCRequest request) { - LSPXWorkspaceManager manager = LSPXWorkspaceManager.getInstance(); + LSPPlugin manager = LSPPlugin.getInstance(); return manager.unhandledMethod(request); } } diff --git a/lsp/src/main/java/lsp/lspx/CTHandler.java b/lsp/src/main/java/lsp/lspx/CTHandler.java index b10799e62..47c846d3a 100644 --- a/lsp/src/main/java/lsp/lspx/CTHandler.java +++ b/lsp/src/main/java/lsp/lspx/CTHandler.java @@ -37,8 +37,8 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.CTPlugin; +import workspace.plugins.LSPPlugin; public class CTHandler extends LSPHandler { @@ -50,7 +50,7 @@ public CTHandler() @Override public RPCMessageList request(RPCRequest request) { - if (!LSPWorkspaceManager.getInstance().hasClientCapability("experimental.combinatorialTesting")) + if (!LSPPlugin.getInstance().hasClientCapability("experimental.combinatorialTesting")) { return new RPCMessageList(request, RPCErrors.MethodNotFound, "CT plugin is not enabled by client"); } @@ -77,7 +77,8 @@ private RPCMessageList traces(RPCRequest request) { JSONObject params = request.get("params"); File project = params == null ? null : Utils.uriToFile(params.get("uri")); - return LSPXWorkspaceManager.getInstance().ctTraces(request, project); + CTPlugin ct = registry.getPlugin("CT"); + return ct.ctTraces(request, project); } catch (URISyntaxException e) { @@ -97,7 +98,8 @@ private RPCMessageList generate(RPCRequest request) { JSONObject params = request.get("params"); String name = params.get("name"); - return LSPXWorkspaceManager.getInstance().ctGenerate(request, name); + CTPlugin ct = registry.getPlugin("CT"); + return ct.ctGenerate(request, name); } catch (Exception e) { @@ -158,7 +160,8 @@ private RPCMessageList execute(RPCRequest request) end = range.get("end"); } - return LSPXWorkspaceManager.getInstance().ctExecute(request, tracename, + CTPlugin ct = registry.getPlugin("CT"); + return ct.ctExecute(request, tracename, partialResultToken, workDoneToken, rType, subset, seed, start, end); } catch (Exception e) diff --git a/lsp/src/main/java/lsp/lspx/POGHandler.java b/lsp/src/main/java/lsp/lspx/POGHandler.java index 7178a5380..5a3e99527 100644 --- a/lsp/src/main/java/lsp/lspx/POGHandler.java +++ b/lsp/src/main/java/lsp/lspx/POGHandler.java @@ -35,8 +35,8 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.LSPPlugin; +import workspace.plugins.POPlugin; public class POGHandler extends LSPHandler { @@ -48,7 +48,7 @@ public POGHandler() @Override public RPCMessageList request(RPCRequest request) { - if (!LSPWorkspaceManager.getInstance().hasClientCapability("experimental.proofObligationGeneration")) + if (!LSPPlugin.getInstance().hasClientCapability("experimental.proofObligationGeneration")) { return new RPCMessageList(request, RPCErrors.MethodNotFound, "PO plugin is not enabled by client"); } @@ -69,7 +69,8 @@ private RPCMessageList generate(RPCRequest request) { JSONObject params = request.get("params"); File file = Utils.uriToFile(params.get("uri")); - return LSPXWorkspaceManager.getInstance().pogGenerate(request, file); + POPlugin po = registry.getPlugin("PO"); + return po.pogGenerate(request, file); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/lspx/TranslateHandler.java b/lsp/src/main/java/lsp/lspx/TranslateHandler.java index 3ac6f3154..9b25080e0 100644 --- a/lsp/src/main/java/lsp/lspx/TranslateHandler.java +++ b/lsp/src/main/java/lsp/lspx/TranslateHandler.java @@ -36,10 +36,10 @@ import rpc.RPCRequest; import workspace.Diag; import workspace.EventHub; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; import workspace.MessageHub; import workspace.events.UnknownTranslationEvent; +import workspace.plugins.LSPPlugin; +import workspace.plugins.TRPlugin; public class TranslateHandler extends LSPHandler { @@ -51,7 +51,7 @@ public TranslateHandler() @Override public RPCMessageList request(RPCRequest request) { - if (!LSPWorkspaceManager.getInstance().hasClientCapability("experimental.translateProvider")) + if (!LSPPlugin.getInstance().hasClientCapability("experimental.translateProvider")) { return new RPCMessageList(request, RPCErrors.MethodNotFound, "Translate capability is not enabled by client"); } @@ -95,19 +95,21 @@ private RPCMessageList translate(RPCRequest request) return new RPCMessageList(request, RPCErrors.InvalidParams, "saveUri does not exist"); } + TRPlugin tr = registry.getPlugin("TR"); + switch (language) { case "latex": - return LSPXWorkspaceManager.getInstance().translateLaTeX(request, file, saveUri, options); + return tr.translateLaTeX(request, file, saveUri, options); case "word": - return LSPXWorkspaceManager.getInstance().translateWord(request, file, saveUri, options); + return tr.translateWord(request, file, saveUri, options); case "coverage": - return LSPXWorkspaceManager.getInstance().translateCoverage(request, file, saveUri, options); + return tr.translateCoverage(request, file, saveUri, options); case "graphviz": - return LSPXWorkspaceManager.getInstance().translateGraphviz(request, file, saveUri, options); + return tr.translateGraphviz(request, file, saveUri, options); default: RPCMessageList result = EventHub.getInstance().publish(new UnknownTranslationEvent(request, language)); diff --git a/lsp/src/main/java/lsp/textdocument/CodeLensHandler.java b/lsp/src/main/java/lsp/textdocument/CodeLensHandler.java index 1f9a83cc0..0ae77d329 100644 --- a/lsp/src/main/java/lsp/textdocument/CodeLensHandler.java +++ b/lsp/src/main/java/lsp/textdocument/CodeLensHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class CodeLensHandler extends LSPHandler { @@ -67,7 +67,7 @@ private RPCMessageList codeLens(RPCRequest request) JSONObject textDocument = params.get("textDocument"); File file = Utils.uriToFile(textDocument.get("uri")); - return LSPWorkspaceManager.getInstance().lspCodeLens(request, file); + return LSPPlugin.getInstance().lspCodeLens(request, file); } catch (URISyntaxException e) { @@ -88,7 +88,7 @@ private RPCMessageList codeLensResolve(RPCRequest request) JSONObject params = request.get("params"); JSONObject data = params.get("data"); - return LSPWorkspaceManager.getInstance().lspCodeLensResolve(request, data); + return LSPPlugin.getInstance().lspCodeLensResolve(request, data); } catch (Exception e) { diff --git a/lsp/src/main/java/lsp/textdocument/CompletionHandler.java b/lsp/src/main/java/lsp/textdocument/CompletionHandler.java index 090f35b0d..2cb2b3589 100644 --- a/lsp/src/main/java/lsp/textdocument/CompletionHandler.java +++ b/lsp/src/main/java/lsp/textdocument/CompletionHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class CompletionHandler extends LSPHandler { @@ -60,7 +60,7 @@ public RPCMessageList request(RPCRequest request) Long line = position.get("line"); Long character = position.get("character"); - return LSPWorkspaceManager.getInstance().lspCompletion(request, triggerKind, file, line, character); + return LSPPlugin.getInstance().lspCompletion(request, triggerKind, file, line, character); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/DefinitionHandler.java b/lsp/src/main/java/lsp/textdocument/DefinitionHandler.java index f62d4c4e1..cd5b48d9f 100644 --- a/lsp/src/main/java/lsp/textdocument/DefinitionHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DefinitionHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DefinitionHandler extends LSPHandler { @@ -56,7 +56,7 @@ public RPCMessageList request(RPCRequest request) Long line = position.get("line"); Long col = position.get("character"); - return LSPWorkspaceManager.getInstance().lspDefinition(request, file, line, col); + return LSPPlugin.getInstance().lspDefinition(request, file, line, col); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/DidChangeHandler.java b/lsp/src/main/java/lsp/textdocument/DidChangeHandler.java index d3ad066d4..1fdabbad2 100644 --- a/lsp/src/main/java/lsp/textdocument/DidChangeHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DidChangeHandler.java @@ -35,7 +35,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DidChangeHandler extends LSPHandler { @@ -63,7 +63,7 @@ public RPCMessageList request(RPCRequest request) JSONObject change = (JSONObject)contentChange; JSONObject range = change.get("range"); String text = change.get("text"); - RPCMessageList r = LSPWorkspaceManager.getInstance().lspDidChange(request, file, range, text); + RPCMessageList r = LSPPlugin.getInstance().lspDidChange(request, file, range, text); if (r != null) result.addAll(r); } } diff --git a/lsp/src/main/java/lsp/textdocument/DidCloseHandler.java b/lsp/src/main/java/lsp/textdocument/DidCloseHandler.java index 51c5cba3c..10bde6794 100644 --- a/lsp/src/main/java/lsp/textdocument/DidCloseHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DidCloseHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DidCloseHandler extends LSPHandler { @@ -52,7 +52,7 @@ public RPCMessageList request(RPCRequest request) JSONObject text = params.get("textDocument"); File file = Utils.uriToFile(text.get("uri")); - return LSPWorkspaceManager.getInstance().lspDidClose(request, file); + return LSPPlugin.getInstance().lspDidClose(request, file); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/DidOpenHandler.java b/lsp/src/main/java/lsp/textdocument/DidOpenHandler.java index 2894af178..f52315034 100644 --- a/lsp/src/main/java/lsp/textdocument/DidOpenHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DidOpenHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DidOpenHandler extends LSPHandler { @@ -53,7 +53,7 @@ public RPCMessageList request(RPCRequest request) File file = Utils.uriToFile(textDoc.get("uri")); String text = textDoc.get("text"); - return LSPWorkspaceManager.getInstance().lspDidOpen(request, file, text); + return LSPPlugin.getInstance().lspDidOpen(request, file, text); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/DidSaveHandler.java b/lsp/src/main/java/lsp/textdocument/DidSaveHandler.java index a10fadd64..24631c9d0 100644 --- a/lsp/src/main/java/lsp/textdocument/DidSaveHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DidSaveHandler.java @@ -33,7 +33,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DidSaveHandler extends LSPHandler { @@ -52,7 +52,7 @@ public RPCMessageList request(RPCRequest request) File file = Utils.uriToFile(textDoc.get("uri")); String text = params.get("text"); - return LSPWorkspaceManager.getInstance().lspDidSave(request, file, text); + return LSPPlugin.getInstance().lspDidSave(request, file, text); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/DocumentSymbolHandler.java b/lsp/src/main/java/lsp/textdocument/DocumentSymbolHandler.java index 24882c248..34ce240ca 100644 --- a/lsp/src/main/java/lsp/textdocument/DocumentSymbolHandler.java +++ b/lsp/src/main/java/lsp/textdocument/DocumentSymbolHandler.java @@ -34,7 +34,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DocumentSymbolHandler extends LSPHandler { @@ -52,7 +52,7 @@ public RPCMessageList request(RPCRequest request) JSONObject textDoc = params.get("textDocument"); File file = Utils.uriToFile(textDoc.get("uri")); - return LSPWorkspaceManager.getInstance().lspDocumentSymbols(request, file); + return LSPPlugin.getInstance().lspDocumentSymbols(request, file); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/lsp/textdocument/ReferencesHandler.java b/lsp/src/main/java/lsp/textdocument/ReferencesHandler.java index 12ec2dc9f..ea26ac4e6 100644 --- a/lsp/src/main/java/lsp/textdocument/ReferencesHandler.java +++ b/lsp/src/main/java/lsp/textdocument/ReferencesHandler.java @@ -33,7 +33,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class ReferencesHandler extends LSPHandler { @@ -58,7 +58,7 @@ public RPCMessageList request(RPCRequest request) JSONObject context = params.get("context"); Boolean incdec = context.get("includeDeclaration"); - return LSPWorkspaceManager.getInstance().lspReferences(request, + return LSPPlugin.getInstance().lspReferences(request, file, line.intValue(), col.intValue(), incdec); } catch (URISyntaxException e) diff --git a/lsp/src/main/java/lsp/textdocument/TypeHierarchyHandler.java b/lsp/src/main/java/lsp/textdocument/TypeHierarchyHandler.java index dda8fd6c7..a6be13c2b 100644 --- a/lsp/src/main/java/lsp/textdocument/TypeHierarchyHandler.java +++ b/lsp/src/main/java/lsp/textdocument/TypeHierarchyHandler.java @@ -37,7 +37,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class TypeHierarchyHandler extends LSPHandler { @@ -82,7 +82,7 @@ private RPCMessageList prepareTypeHierarchy(RPCRequest request) Long line = position.get("line"); Long col = position.get("character"); - return LSPWorkspaceManager.getInstance().lspPrepareTypeHierarchy(request, file, line, col); + return LSPPlugin.getInstance().lspPrepareTypeHierarchy(request, file, line, col); } catch (URISyntaxException e) { @@ -104,7 +104,7 @@ private RPCMessageList supertypes(RPCRequest request) JSONObject item = params.get("item"); String classname = item.get("name"); - return LSPWorkspaceManager.getInstance().lspSupertypes(request, classname); + return LSPPlugin.getInstance().lspSupertypes(request, classname); } catch (Exception e) { @@ -122,7 +122,7 @@ private RPCMessageList subtypes(RPCRequest request) JSONObject item = params.get("item"); String classname = item.get("name"); - return LSPWorkspaceManager.getInstance().lspSubtypes(request, classname); + return LSPPlugin.getInstance().lspSubtypes(request, classname); } catch (Exception e) { diff --git a/lsp/src/main/java/lsp/workspace/DidChangeWSHandler.java b/lsp/src/main/java/lsp/workspace/DidChangeWSHandler.java index b8c46d2d1..5f54969ff 100644 --- a/lsp/src/main/java/lsp/workspace/DidChangeWSHandler.java +++ b/lsp/src/main/java/lsp/workspace/DidChangeWSHandler.java @@ -38,7 +38,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; public class DidChangeWSHandler extends LSPHandler { @@ -80,7 +80,7 @@ private RPCMessageList didChangeWatchedFiles(RPCRequest request) { WatchKind type = WatchKind.kindOf(change.get("type")); File file = Utils.uriToFile(uri); - int code = LSPWorkspaceManager.getInstance().lspDidChangeWatchedFile(request, file, type); + int code = LSPPlugin.getInstance().lspDidChangeWatchedFile(request, file, type); if (code > actionCode) // Note: ordered severity { @@ -102,7 +102,7 @@ private RPCMessageList didChangeWatchedFiles(RPCRequest request) // Do rebuilding and type checking after ALL the changes are processed // This can return null, since didChangeWatchedFiles is a notification. - return LSPWorkspaceManager.getInstance().afterChangeWatchedFiles(request, actionCode, deleted); + return LSPPlugin.getInstance().afterChangeWatchedFiles(request, actionCode, deleted); } catch (URISyntaxException e) { diff --git a/lsp/src/main/java/vdmj/DAPDebugLink.java b/lsp/src/main/java/vdmj/DAPDebugLink.java index 1964806c6..2ff2c229b 100644 --- a/lsp/src/main/java/vdmj/DAPDebugLink.java +++ b/lsp/src/main/java/vdmj/DAPDebugLink.java @@ -44,8 +44,8 @@ import dap.DAPResponse; import dap.DAPServer; import json.JSONObject; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; public class DAPDebugLink extends ConsoleDebugLink { @@ -103,7 +103,7 @@ public void newThread(CPUValue cpu) return; // Too late! } - if (DAPWorkspaceManager.getInstance().getNoDebug()) + if (DAPPlugin.getInstance().getNoDebug()) { return; // No one cares } @@ -238,7 +238,7 @@ public void complete(DebugReason reason, ContextException exception) return; // Too late! } - if (DAPWorkspaceManager.getInstance().getNoDebug()) + if (DAPPlugin.getInstance().getNoDebug()) { return; // No one cares } diff --git a/lsp/src/main/java/vdmj/DAPDebugReader.java b/lsp/src/main/java/vdmj/DAPDebugReader.java index b76f74853..312ecc088 100644 --- a/lsp/src/main/java/vdmj/DAPDebugReader.java +++ b/lsp/src/main/java/vdmj/DAPDebugReader.java @@ -46,8 +46,8 @@ import json.JSONArray; import json.JSONObject; import lsp.Utils; -import workspace.DAPWorkspaceManager; import workspace.Diag; +import workspace.plugins.DAPPlugin; /** * A class to listen for and interact with multiple threads that are being debugged. @@ -147,7 +147,7 @@ private boolean doCommand() throws Exception JSONObject source = arguments.get("source"); File file = Utils.pathToFile(source.get("path")); JSONArray lines = arguments.get("breakpoints"); - DAPMessageList responses = DAPWorkspaceManager.getInstance().dapSetBreakpoints(dapRequest, file, lines); + DAPMessageList responses = DAPPlugin.getInstance().dapSetBreakpoints(dapRequest, file, lines); for (JSONObject response: responses) { @@ -162,7 +162,7 @@ private boolean doCommand() throws Exception { JSONObject arguments = dapRequest.get("arguments"); JSONArray names = arguments.get("breakpoints"); - DAPMessageList responses = DAPWorkspaceManager.getInstance().dapSetFunctionBreakpoints(dapRequest, names); + DAPMessageList responses = DAPPlugin.getInstance().dapSetFunctionBreakpoints(dapRequest, names); for (JSONObject response: responses) { @@ -177,7 +177,7 @@ private boolean doCommand() throws Exception { JSONObject arguments = dapRequest.get("arguments"); JSONArray filterOptions = arguments.get("filterOptions"); - DAPMessageList responses = DAPWorkspaceManager.getInstance().dapSetExceptionBreakpoints(dapRequest, filterOptions); + DAPMessageList responses = DAPPlugin.getInstance().dapSetExceptionBreakpoints(dapRequest, filterOptions); for (JSONObject response: responses) { diff --git a/lsp/src/main/java/vdmj/commands/GenerateCommand.java b/lsp/src/main/java/vdmj/commands/GenerateCommand.java index 900bce807..35da5994f 100644 --- a/lsp/src/main/java/vdmj/commands/GenerateCommand.java +++ b/lsp/src/main/java/vdmj/commands/GenerateCommand.java @@ -33,9 +33,9 @@ import dap.GenerateExecutor; import lsp.LSPException; import lsp.Utils; -import workspace.DAPWorkspaceManager; import workspace.Diag; import workspace.PluginRegistry; +import workspace.plugins.DAPPlugin; import workspace.plugins.INPlugin; public class GenerateCommand extends AnalysisCommand @@ -69,7 +69,7 @@ public DAPMessageList run(DAPRequest request) return new DAPMessageList(request, false, "Specification has changed: try restart", null); } - Interpreter interpreter = DAPWorkspaceManager.getInstance().getInterpreter(); + Interpreter interpreter = DAPPlugin.getInstance().getInterpreter(); interpreter.init(); TCNameToken qname = null; diff --git a/lsp/src/main/java/vdmj/commands/InitCommand.java b/lsp/src/main/java/vdmj/commands/InitCommand.java index 358c14f49..1b54e7108 100644 --- a/lsp/src/main/java/vdmj/commands/InitCommand.java +++ b/lsp/src/main/java/vdmj/commands/InitCommand.java @@ -33,7 +33,7 @@ import dap.DAPResponse; import dap.InitExecutor; import json.JSONObject; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class InitCommand extends AnalysisCommand implements ScriptRunnable { @@ -92,7 +92,7 @@ public boolean notWhenRunning() public String scriptRun(DAPRequest request) throws IOException { LexLocation.clearLocations(); - DAPWorkspaceManager.getInstance().getInterpreter().init(); + DAPPlugin.getInstance().getInterpreter().init(); return "()\nGlobal context initialized\nCleared all coverage information"; } } diff --git a/lsp/src/main/java/vdmj/commands/PrintCommand.java b/lsp/src/main/java/vdmj/commands/PrintCommand.java index 09abe77c9..f1636c646 100644 --- a/lsp/src/main/java/vdmj/commands/PrintCommand.java +++ b/lsp/src/main/java/vdmj/commands/PrintCommand.java @@ -29,7 +29,7 @@ import dap.DAPMessageList; import dap.DAPRequest; import dap.ExpressionExecutor; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class PrintCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable { @@ -66,7 +66,7 @@ public String initRun(DAPRequest request) { try { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); return manager.getInterpreter().execute(expression).toString(); } catch (Exception e) diff --git a/lsp/src/main/java/vdmj/commands/QuitCommand.java b/lsp/src/main/java/vdmj/commands/QuitCommand.java index 4731739c2..9bcdf60f6 100644 --- a/lsp/src/main/java/vdmj/commands/QuitCommand.java +++ b/lsp/src/main/java/vdmj/commands/QuitCommand.java @@ -28,7 +28,7 @@ import dap.DAPRequest; import dap.DAPServer; import lsp.CancellableThread; -import workspace.DAPWorkspaceManager; +import workspace.plugins.DAPPlugin; public class QuitCommand extends AnalysisCommand { @@ -48,7 +48,7 @@ public QuitCommand(String line) @Override public DAPMessageList run(DAPRequest request) { - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); if (CancellableThread.currentlyRunning() != null) { diff --git a/lsp/src/main/java/vdmj/commands/RuntraceCommand.java b/lsp/src/main/java/vdmj/commands/RuntraceCommand.java index e078fff81..839bc553b 100644 --- a/lsp/src/main/java/vdmj/commands/RuntraceCommand.java +++ b/lsp/src/main/java/vdmj/commands/RuntraceCommand.java @@ -30,10 +30,10 @@ import json.JSONObject; import lsp.LSPException; import lsp.Utils; -import workspace.DAPWorkspaceManager; import workspace.Diag; import workspace.PluginRegistry; import workspace.plugins.CTPlugin; +import workspace.plugins.DAPPlugin; public class RuntraceCommand extends AnalysisCommand implements InitRunnable { @@ -69,7 +69,7 @@ public String initRun(DAPRequest request) { try { - DAPWorkspaceManager dapManager = DAPWorkspaceManager.getInstance(); + DAPPlugin dapManager = DAPPlugin.getInstance(); CTPlugin ct = PluginRegistry.getInstance().getPlugin("CT"); if (ct.isRunning()) diff --git a/lsp/src/main/java/workspace/DAPXWorkspaceManager.java b/lsp/src/main/java/workspace/DAPXWorkspaceManager.java deleted file mode 100644 index d6af41f95..000000000 --- a/lsp/src/main/java/workspace/DAPXWorkspaceManager.java +++ /dev/null @@ -1,77 +0,0 @@ -/******************************************************************************* - * - * Copyright (c) 2022 Nick Battle. - * - * Author: Nick Battle - * - * This file is part of VDMJ. - * - * VDMJ is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * VDMJ is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with VDMJ. If not, see . - * SPDX-License-Identifier: GPL-3.0-or-later - * - ******************************************************************************/ - -package workspace; - -import dap.DAPMessageList; -import dap.DAPRequest; -import workspace.events.UnknownCommandEvent; - -public class DAPXWorkspaceManager -{ - private static DAPXWorkspaceManager INSTANCE = null; - private final EventHub eventhub; - - protected DAPXWorkspaceManager() - { - this.eventhub = EventHub.getInstance(); - Diag.info("Created DAPXWorkspaceManager"); - } - - public static synchronized DAPXWorkspaceManager getInstance() - { - if (INSTANCE == null) - { - INSTANCE = new DAPXWorkspaceManager(); - } - - return INSTANCE; - } - - /** - * This is only used by unit testing. - */ - public static void reset() - { - if (INSTANCE != null) - { - INSTANCE = null; - } - } - - public DAPMessageList unhandledCommand(DAPRequest request) - { - DAPMessageList responses = eventhub.publish(new UnknownCommandEvent(request)); - - if (responses.isEmpty()) - { - Diag.error("No external plugin registered for unknownMethodEvent (%s)", request.getCommand()); - return new DAPMessageList(request, false, "Unknown DAP command: " + request.getCommand(), null); - } - else - { - return responses; - } - } -} diff --git a/lsp/src/main/java/workspace/EventListener.java b/lsp/src/main/java/workspace/EventListener.java index 7ec085634..330ea344f 100644 --- a/lsp/src/main/java/workspace/EventListener.java +++ b/lsp/src/main/java/workspace/EventListener.java @@ -34,12 +34,16 @@ */ public interface EventListener { + public final static int LSP_PRIORITY = Integer.getInteger("lspx.plugins.priority.lsp", 0); + public final static int DAP_PRIORITY = Integer.getInteger("lspx.plugins.priority.dap", 0); + public final static int WS_PRIORITY = Integer.getInteger("lspx.plugins.priority.ws", 100); public final static int AST_PRIORITY = Integer.getInteger("lspx.plugins.priority.ast", 200); public final static int TC_PRIORITY = Integer.getInteger("lspx.plugins.priority.tc", 300); public final static int IN_PRIORITY = Integer.getInteger("lspx.plugins.priority.in", 400); public final static int PO_PRIORITY = Integer.getInteger("lspx.plugins.priority.po", 500); public final static int CT_PRIORITY = Integer.getInteger("lspx.plugins.priority.co", 600); + public final static int TR_PRIORITY = Integer.getInteger("lspx.plugins.priority.tr", 700); public final static int USER_PRIORITY = Integer.getInteger("lspx.plugins.priority.user", 1000); diff --git a/lsp/src/main/java/workspace/MessageHub.java b/lsp/src/main/java/workspace/MessageHub.java index 160b50e70..96e6bd48e 100644 --- a/lsp/src/main/java/workspace/MessageHub.java +++ b/lsp/src/main/java/workspace/MessageHub.java @@ -40,6 +40,7 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.plugins.AnalysisPlugin; +import workspace.plugins.LSPPlugin; /** * A singleton object to manage the current set of error and warning messages for all @@ -226,7 +227,7 @@ public synchronized void clear() */ public RPCMessageList getDiagnosticResponses() { - Set files = LSPWorkspaceManager.getInstance().getProjectFiles().keySet(); + Set files = LSPPlugin.getInstance().getProjectFiles().keySet(); return getDiagnosticResponses(files); } diff --git a/lsp/src/main/java/workspace/lenses/CodeLens.java b/lsp/src/main/java/workspace/lenses/CodeLens.java index 2fe07ecf2..83f68817a 100644 --- a/lsp/src/main/java/workspace/lenses/CodeLens.java +++ b/lsp/src/main/java/workspace/lenses/CodeLens.java @@ -29,7 +29,7 @@ import json.JSONObject; import lsp.Utils; import workspace.Diag; -import workspace.LSPWorkspaceManager; +import workspace.plugins.LSPPlugin; /** * The base class for all code lenses. @@ -43,7 +43,7 @@ abstract public class CodeLens */ protected String getClientName() { - return LSPWorkspaceManager.getInstance().getClientInfo("name"); + return LSPPlugin.getInstance().getClientInfo("name"); } /** diff --git a/lsp/src/main/java/workspace/plugins/ASTPlugin.java b/lsp/src/main/java/workspace/plugins/ASTPlugin.java index 99bdc70ed..a15b6ff98 100644 --- a/lsp/src/main/java/workspace/plugins/ASTPlugin.java +++ b/lsp/src/main/java/workspace/plugins/ASTPlugin.java @@ -53,7 +53,6 @@ import rpc.RPCRequest; import workspace.Diag; import workspace.EventListener; -import workspace.LSPWorkspaceManager; import workspace.events.ChangeFileEvent; import workspace.events.CheckPrepareEvent; import workspace.events.CheckSyntaxEvent; @@ -149,7 +148,7 @@ else if (event instanceof CheckSyntaxEvent) private RPCMessageList lspDynamicRegistrations() { RPCMessageList registrations = new RPCMessageList(); - LSPWorkspaceManager manager = LSPWorkspaceManager.getInstance(); + LSPPlugin manager = LSPPlugin.getInstance(); if (manager.hasClientCapability("workspace.didChangeWatchedFiles.dynamicRegistration")) { diff --git a/lsp/src/main/java/workspace/plugins/ASTPluginPR.java b/lsp/src/main/java/workspace/plugins/ASTPluginPR.java index 891a79375..789cd7c4d 100644 --- a/lsp/src/main/java/workspace/plugins/ASTPluginPR.java +++ b/lsp/src/main/java/workspace/plugins/ASTPluginPR.java @@ -46,7 +46,6 @@ import json.JSONArray; import lsp.textdocument.SymbolKind; import workspace.Diag; -import workspace.LSPWorkspaceManager; import workspace.events.CheckPrepareEvent; import workspace.events.CheckSyntaxEvent; import workspace.lenses.ASTCodeLens; @@ -74,7 +73,7 @@ public void checkLoadedFiles(CheckSyntaxEvent event) dirty = false; dirtyClassList = null; - Map projectFiles = LSPWorkspaceManager.getInstance().getProjectFiles(); + Map projectFiles = LSPPlugin.getInstance().getProjectFiles(); LexLocation.resetLocations(); if (Settings.dialect == Dialect.VDM_RT) @@ -147,7 +146,7 @@ protected void parseFile(File file) { dirty = true; // Until saved. - Map projectFiles = LSPWorkspaceManager.getInstance().getProjectFiles(); + Map projectFiles = LSPPlugin.getInstance().getProjectFiles(); StringBuilder buffer = projectFiles.get(file); LexTokenReader ltr = new LexTokenReader(buffer.toString(), Settings.dialect, file); diff --git a/lsp/src/main/java/workspace/plugins/ASTPluginSL.java b/lsp/src/main/java/workspace/plugins/ASTPluginSL.java index ac530147a..1b659549e 100644 --- a/lsp/src/main/java/workspace/plugins/ASTPluginSL.java +++ b/lsp/src/main/java/workspace/plugins/ASTPluginSL.java @@ -42,7 +42,6 @@ import json.JSONArray; import lsp.textdocument.SymbolKind; -import workspace.LSPWorkspaceManager; import workspace.events.CheckPrepareEvent; import workspace.events.CheckSyntaxEvent; import workspace.lenses.ASTCodeLens; @@ -68,7 +67,7 @@ protected void preCheck(CheckPrepareEvent ev) public void checkLoadedFiles(CheckSyntaxEvent event) { dirty = false; - Map projectFiles = LSPWorkspaceManager.getInstance().getProjectFiles(); + Map projectFiles = LSPPlugin.getInstance().getProjectFiles(); LexLocation.resetLocations(); for (Entry entry: projectFiles.entrySet()) @@ -102,7 +101,7 @@ protected void parseFile(File file) dirty = true; // Until saved. dirtyModuleList = null; - Map projectFiles = LSPWorkspaceManager.getInstance().getProjectFiles(); + Map projectFiles = LSPPlugin.getInstance().getProjectFiles(); StringBuilder buffer = projectFiles.get(file); LexTokenReader ltr = new LexTokenReader(buffer.toString(), Settings.dialect, file); diff --git a/lsp/src/main/java/workspace/plugins/AnalysisPlugin.java b/lsp/src/main/java/workspace/plugins/AnalysisPlugin.java index 228eb343d..074da741c 100644 --- a/lsp/src/main/java/workspace/plugins/AnalysisPlugin.java +++ b/lsp/src/main/java/workspace/plugins/AnalysisPlugin.java @@ -26,9 +26,11 @@ import com.fujitsu.vdmj.plugins.HelpList; +import dap.DAPDispatcher; import dap.DAPMessageList; import json.JSONObject; import lsp.LSPMessageUtils; +import rpc.RPCDispatcher; import rpc.RPCErrors; import rpc.RPCMessageList; import vdmj.commands.AnalysisCommand; @@ -41,6 +43,8 @@ abstract public class AnalysisPlugin { + protected final RPCDispatcher lspDispatcher; + protected final DAPDispatcher dapDispatcher; protected final LSPMessageUtils messages; protected final PluginRegistry registry; protected final EventHub eventhub; @@ -48,6 +52,8 @@ abstract public class AnalysisPlugin public AnalysisPlugin() { + lspDispatcher = RPCDispatcher.getInstance(); + dapDispatcher = DAPDispatcher.getInstance(); messages = new LSPMessageUtils(); registry = PluginRegistry.getInstance(); eventhub = EventHub.getInstance(); diff --git a/lsp/src/main/java/workspace/plugins/CTPlugin.java b/lsp/src/main/java/workspace/plugins/CTPlugin.java index 50cd9b5c8..f58b2a614 100644 --- a/lsp/src/main/java/workspace/plugins/CTPlugin.java +++ b/lsp/src/main/java/workspace/plugins/CTPlugin.java @@ -24,6 +24,7 @@ package workspace.plugins; +import java.io.File; import java.io.IOException; import java.util.List; import java.util.Map; @@ -50,12 +51,13 @@ import lsp.CancellableThread; import lsp.LSPException; import lsp.LSPServer; +import lsp.Utils; +import lsp.lspx.CTHandler; import rpc.RPCErrors; import rpc.RPCMessageList; import rpc.RPCRequest; import rpc.RPCResponse; import vdmj.commands.GenerateCommand; -import workspace.DAPWorkspaceManager; import workspace.Diag; import workspace.EventListener; import workspace.events.CheckCompleteEvent; @@ -116,6 +118,8 @@ public int getPriority() @Override public void init() { + lspDispatcher.register(new CTHandler(), "slsp/CT/traces", "slsp/CT/generate", "slsp/CT/execute"); + eventhub.register(CheckPrepareEvent.class, this); eventhub.register(CheckCompleteEvent.class, this); eventhub.register(DAPBeforeEvaluateEvent.class, this); @@ -201,9 +205,129 @@ public HelpList getCommandHelp() abstract public T getCT(); + + public RPCMessageList ctTraces(RPCRequest request, File project) + { + try + { + if (messagehub.hasErrors()) + { + return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); + } + + DAPPlugin.getInstance().refreshInterpreter(); + CTPlugin ct = registry.getPlugin("CT"); + Map nameMap = ct.getTraceNames(); + JSONArray results = new JSONArray(); + + for (String module: nameMap.keySet()) + { + JSONArray array = new JSONArray(); + + for (TCNameToken name: nameMap.get(module)) + { + array.add(new JSONObject( + "name", name.getExplicit(true).toString(), + "location", Utils.lexLocationToLocation(name.getLocation()))); + } + + results.add(new JSONObject("name", module, "traces", array)); + } + + return new RPCMessageList(request, results); + } + catch (Exception e) + { + Diag.error(e); + return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); + } + } + + public RPCMessageList ctGenerate(RPCRequest request, String name) + { + try + { + if (messagehub.hasErrors()) + { + return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); + } + + CTPlugin ct = registry.getPlugin("CT"); + + if (ct.isRunning()) + { + return new RPCMessageList(request, RPCErrors.InvalidRequest, "Trace still running"); + } + + DAPPlugin.getInstance().refreshInterpreter(); + TCNameToken tracename = Utils.stringToName(name); + int count = ct.generate(tracename); + return new RPCMessageList(request, new JSONObject("numberOfTests", count)); + } + catch (LSPException e) + { + Diag.error(e); + return new RPCMessageList(request, e.getError(), e.getMessage()); + } + catch (Exception e) + { + Diag.error(e); + return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); + } + } + + public RPCMessageList ctExecute(RPCRequest request, String name, + Object progressToken, Object workDoneToken, + TraceReductionType rType, float subset, long seed, Long start, Long end) + { + try + { + if (messagehub.hasErrors()) + { + return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); + } + + TCNameToken tracename = Utils.stringToName(name); + CTPlugin ct = registry.getPlugin("CT"); + + if (ct.isRunning()) + { + return new RPCMessageList(request, RPCErrors.InvalidRequest, "Trace still running"); + } + + if (DAPPlugin.getInstance().refreshInterpreter()) + { + Diag.error("The spec has changed since generate, so re-generating"); + ct.generate(tracename); + } + + JSONArray batch = ct.runTraceRange(request, tracename, progressToken, workDoneToken, + rType, subset, seed, start, end); + + if (batch == null) // Running in background + { + return null; + } + else + { + return new RPCMessageList(request, batch); + } + } + catch (LSPException e) + { + Diag.error(e); + return new RPCMessageList(request, e.getError(), e.getMessage()); + } + catch (Exception e) + { + Diag.error(e); + return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); + } + } + public int generate(TCNameToken tracename) throws LSPException { - Interpreter interpreter = DAPWorkspaceManager.getInstance().getInterpreter(); + Interpreter interpreter = DAPPlugin.getInstance().getInterpreter(); interpreter.init(); INNamedTraceDefinition tracedef = interpreter.findTraceDefinition(tracename); @@ -313,7 +437,7 @@ public JSONObject runOneTrace(TCNameToken tracename, long testNumber) throws LSP CallSequence test = traceIterator.getNextTest(); String callString = test.getCallString(traceContext); - Interpreter interpreter = DAPWorkspaceManager.getInstance().getInterpreter(); + Interpreter interpreter = DAPPlugin.getInstance().getInterpreter(); // interpreter.init(); Not needed as we run from InitExecutor only List result = interpreter.runOneTrace(traceClassDef, test, true); @@ -465,7 +589,7 @@ private void send(LSPServer server, JSONObject response) throws IOException private JSONArray runBatch(int batchSize, long endTest) throws Exception { - Interpreter interpreter = DAPWorkspaceManager.getInstance().getInterpreter(); + Interpreter interpreter = DAPPlugin.getInstance().getInterpreter(); JSONArray array = new JSONArray(); Diag.fine("Starting batch at test number %d...", testNumber); diff --git a/lsp/src/main/java/workspace/DAPWorkspaceManager.java b/lsp/src/main/java/workspace/plugins/DAPPlugin.java similarity index 90% rename from lsp/src/main/java/workspace/DAPWorkspaceManager.java rename to lsp/src/main/java/workspace/plugins/DAPPlugin.java index d67d58296..f13b421bd 100644 --- a/lsp/src/main/java/workspace/DAPWorkspaceManager.java +++ b/lsp/src/main/java/workspace/plugins/DAPPlugin.java @@ -22,7 +22,7 @@ * ******************************************************************************/ -package workspace; +package workspace.plugins; import java.io.File; import java.io.IOException; @@ -71,12 +71,27 @@ import dap.DAPServer; import dap.InitExecutor; import dap.RemoteControlExecutor; +import dap.UnknownHandler; +import dap.handlers.DebuggingHandler; +import dap.handlers.DisconnectHandler; +import dap.handlers.EvaluateHandler; +import dap.handlers.InitializeHandler; +import dap.handlers.LaunchHandler; +import dap.handlers.PauseHandler; +import dap.handlers.SetBreakpointsHandler; +import dap.handlers.SourceHandler; +import dap.handlers.StackTraceHandler; +import dap.handlers.TerminateHandler; +import dap.handlers.ThreadsHandler; import json.JSONArray; import json.JSONObject; import lsp.CancellableThread; import lsp.Utils; import vdmj.DAPDebugReader; import vdmj.commands.AnalysisCommand; +import workspace.Diag; +import workspace.EventListener; +import workspace.PluginRegistry; import workspace.events.DAPBeforeEvaluateEvent; import workspace.events.DAPConfigDoneEvent; import workspace.events.DAPDisconnectEvent; @@ -84,15 +99,11 @@ import workspace.events.DAPInitializeEvent; import workspace.events.DAPLaunchEvent; import workspace.events.DAPTerminateEvent; -import workspace.plugins.ASTPlugin; -import workspace.plugins.INPlugin; +import workspace.events.UnknownCommandEvent; -public class DAPWorkspaceManager +public class DAPPlugin extends AnalysisPlugin { - private static DAPWorkspaceManager INSTANCE = null; - private final PluginRegistry registry; - private final EventHub eventhub; - private final MessageHub messagehub; + private static DAPPlugin INSTANCE = null; private JSONObject clientCapabilities; private Boolean noDebug; @@ -120,24 +131,57 @@ public class DAPWorkspaceManager "vdmj.in.typebind_limit" ); - protected DAPWorkspaceManager() + protected DAPPlugin() { - this.registry = PluginRegistry.getInstance(); - this.eventhub = EventHub.getInstance(); - this.messagehub = MessageHub.getInstance(); - Diag.info("Created DAPWorkspaceManager"); + Diag.info("DAPPlugin created"); + } + + @Override + public int getPriority() + { + return EventListener.DAP_PRIORITY; + } + + @Override + public String getName() + { + return "DAP"; } - public static synchronized DAPWorkspaceManager getInstance() + public static synchronized DAPPlugin getInstance() { if (INSTANCE == null) { - INSTANCE = new DAPWorkspaceManager(); + INSTANCE = new DAPPlugin(); + + PluginRegistry registry = PluginRegistry.getInstance(); + registry.registerPlugin(INSTANCE); } return INSTANCE; } + @Override + public void init() + { + dapDispatcher.register(new InitializeHandler(), "initialize"); + dapDispatcher.register(new LaunchHandler(), "launch"); + dapDispatcher.register(new InitializeHandler(), "configurationDone"); + dapDispatcher.register(new ThreadsHandler(), "threads"); + dapDispatcher.register(new SetBreakpointsHandler(), "setBreakpoints", "setExceptionBreakpoints", "setFunctionBreakpoints"); + dapDispatcher.register(new EvaluateHandler(), "evaluate"); + dapDispatcher.register(new StackTraceHandler(), "stackTrace"); + dapDispatcher.register(new DisconnectHandler(), "disconnect"); + dapDispatcher.register(new TerminateHandler(), "terminate"); + dapDispatcher.register(new PauseHandler(), "pause"); + dapDispatcher.register(new SourceHandler(), "source"); + + dapDispatcher.register(new DebuggingHandler(), + "continue", "stepIn", "stepOut", "next", "scopes", "variables"); + + dapDispatcher.register(new UnknownHandler()); + } + /** * This is only used by unit testing. */ @@ -166,7 +210,7 @@ public DAPMessageList dapInitialize(DAPRequest request, JSONObject clientCapabil public DAPMessageList dapLaunch(DAPRequest request, boolean noDebug, String defaultName, String command, String remoteControl, String logging) throws Exception { - LSPWorkspaceManager manager = LSPWorkspaceManager.getInstance(); + LSPPlugin manager = LSPPlugin.getInstance(); if (manager.checkInProgress()) { @@ -282,8 +326,8 @@ private void processSettings(DAPRequest request) } // System properties above override those from any properties file - Diag.info("Reading properties from %s", LSPWorkspaceManager.PROPERTIES); - Properties.init(LSPWorkspaceManager.PROPERTIES); + Diag.info("Reading properties from %s", LSPPlugin.PROPERTIES); + Properties.init(LSPPlugin.PROPERTIES); } } @@ -308,8 +352,8 @@ private void restoreSettings() } // Reset properties from the file - Diag.info("Resetting properties from %s", LSPWorkspaceManager.PROPERTIES); - Properties.init(LSPWorkspaceManager.PROPERTIES); + Diag.info("Resetting properties from %s", LSPPlugin.PROPERTIES); + Properties.init(LSPPlugin.PROPERTIES); } public DAPMessageList dapConfigurationDone(DAPRequest request) @@ -374,6 +418,21 @@ public T getClientCapability(String dotName) } } + public DAPMessageList unhandledCommand(DAPRequest request) + { + DAPMessageList responses = eventhub.publish(new UnknownCommandEvent(request)); + + if (responses.isEmpty()) + { + Diag.error("No external plugin registered for unknownMethodEvent (%s)", request.getCommand()); + return new DAPMessageList(request, false, "Unknown DAP command: " + request.getCommand(), null); + } + else + { + return responses; + } + } + /** * The interpreter has changed if there is an interpreter, and the IN tree * within that interpreter is not the same as the IN plugin's tree. @@ -851,7 +910,7 @@ public DAPMessageList dapTerminate(DAPRequest request, Boolean restart) if (restart && !specHasErrors()) { stdout("\nSession restarting...\n"); - LSPWorkspaceManager lsp = LSPWorkspaceManager.getInstance(); + LSPPlugin lsp = LSPPlugin.getInstance(); lsp.restart(); } else diff --git a/lsp/src/main/java/workspace/LSPWorkspaceManager.java b/lsp/src/main/java/workspace/plugins/LSPPlugin.java similarity index 86% rename from lsp/src/main/java/workspace/LSPWorkspaceManager.java rename to lsp/src/main/java/workspace/plugins/LSPPlugin.java index f8cd408c2..0bbd47649 100644 --- a/lsp/src/main/java/workspace/LSPWorkspaceManager.java +++ b/lsp/src/main/java/workspace/plugins/LSPPlugin.java @@ -22,7 +22,7 @@ * ******************************************************************************/ -package workspace; +package workspace.plugins; import java.io.BufferedReader; import java.io.File; @@ -32,6 +32,9 @@ import java.io.IOException; import java.io.InputStreamReader; import java.io.PrintWriter; +import java.lang.reflect.Constructor; +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; import java.net.URI; import java.nio.charset.Charset; import java.nio.file.Files; @@ -54,6 +57,7 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.config.Properties; import com.fujitsu.vdmj.lex.BacktrackInputReader; +import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.runtime.SourceFile; @@ -68,19 +72,43 @@ import com.fujitsu.vdmj.tc.types.TCRecordType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; +import com.fujitsu.vdmj.util.GetResource; import json.JSONArray; import json.JSONObject; +import lsp.CancelHandler; +import lsp.ExitHandler; +import lsp.InitializeHandler; import lsp.LSPInitializeResponse; -import lsp.LSPMessageUtils; import lsp.LSPServer; +import lsp.SetTraceNotificationHandler; +import lsp.ShutdownHandler; +import lsp.UnknownHandler; import lsp.Utils; +import lsp.textdocument.CodeLensHandler; +import lsp.textdocument.CompletionHandler; import lsp.textdocument.CompletionItemKind; import lsp.textdocument.CompletionTriggerKind; +import lsp.textdocument.DefinitionHandler; +import lsp.textdocument.DidChangeHandler; +import lsp.textdocument.DidCloseHandler; +import lsp.textdocument.DidOpenHandler; +import lsp.textdocument.DidSaveHandler; +import lsp.textdocument.DocumentSymbolHandler; +import lsp.textdocument.ReferencesHandler; +import lsp.textdocument.TypeHierarchyHandler; import lsp.textdocument.WatchKind; +import lsp.workspace.DidChangeWSHandler; import rpc.RPCErrors; import rpc.RPCMessageList; import rpc.RPCRequest; +import workspace.Diag; +import workspace.DiagUtils; +import workspace.EventHub; +import workspace.EventListener; +import workspace.GlobFinder; +import workspace.MessageHub; +import workspace.PluginRegistry; import workspace.events.ChangeFileEvent; import workspace.events.CheckCompleteEvent; import workspace.events.CheckFailedEvent; @@ -95,18 +123,15 @@ import workspace.events.OpenFileEvent; import workspace.events.SaveFileEvent; import workspace.events.ShutdownEvent; -import workspace.plugins.ASTPlugin; -import workspace.plugins.INPlugin; -import workspace.plugins.TCPlugin; -import workspace.plugins.WSPlugin; +import workspace.events.UnknownMethodEvent; -public class LSPWorkspaceManager +/** + * The main AnalysisPlugin that deals with LSP protocol messages. This is + * created at startup by the LSP listener. + */ +public class LSPPlugin extends AnalysisPlugin { - private static LSPWorkspaceManager INSTANCE = null; - private PluginRegistry registry; - private EventHub eventhub; - private MessageHub messagehub; - private final LSPMessageUtils msgutils; + private static LSPPlugin INSTANCE = null; private final Charset encoding; private JSONObject clientInfo; @@ -129,54 +154,87 @@ public class LSPWorkspaceManager private static final String EXTERNALS = ".vscode/externals"; public static final String PROPERTIES = ".vscode/vdmj.properties"; - private LSPWorkspaceManager() + private LSPPlugin() { - registry = PluginRegistry.getInstance(); - eventhub = EventHub.getInstance(); - messagehub = MessageHub.getInstance(); - msgutils = new LSPMessageUtils(); - if (System.getProperty("lsp.encoding") == null) { encoding = Charset.defaultCharset(); - Diag.info("Workspace created, using default encoding: %s", encoding.name()); + Diag.info("LSPPlugin created, using default encoding: %s", encoding.name()); } else { encoding = Charset.forName(System.getProperty("lsp.encoding")); - Diag.info("Workspace created, encoding set to %s", encoding.displayName()); + Diag.info("LSPPlugin created, encoding set to %s", encoding.displayName()); } } + + @Override + public int getPriority() + { + return EventListener.LSP_PRIORITY; + } - public static synchronized LSPWorkspaceManager getInstance() + @Override + public String getName() + { + return "LSP"; + } + + public static synchronized LSPPlugin getInstance() { if (INSTANCE == null) { - INSTANCE = new LSPWorkspaceManager(); + INSTANCE = new LSPPlugin(); /** - * Register the built-in plugins. Others are registered in LSPXWorkspaceManager, - * when the client capabilities have been received. + * Register the built-in plugins. Others are registered when the client capabilities + * have been received. */ PluginRegistry registry = PluginRegistry.getInstance(); + + registry.registerPlugin(INSTANCE); registry.registerPlugin(WSPlugin.factory(Settings.dialect)); registry.registerPlugin(ASTPlugin.factory(Settings.dialect)); registry.registerPlugin(TCPlugin.factory(Settings.dialect)); registry.registerPlugin(INPlugin.factory(Settings.dialect)); + registry.registerPlugin(TRPlugin.factory(Settings.dialect)); - Diag.info("Created LSPWorkspaceManager"); + Diag.info("Created LSPPlugin"); } return INSTANCE; } - + + @Override + public void init() + { + lspDispatcher.register(new InitializeHandler(), "initialize", "initialized", "client/registerCapability"); + lspDispatcher.register(new ShutdownHandler(), "shutdown"); + lspDispatcher.register(new ExitHandler(), "exit"); + lspDispatcher.register(new CancelHandler(), "$/cancelRequest"); + lspDispatcher.register(new SetTraceNotificationHandler(), "$/setTraceNotification", "$/setTrace"); + + lspDispatcher.register(new DidOpenHandler(), "textDocument/didOpen"); + lspDispatcher.register(new DidCloseHandler(), "textDocument/didClose"); + lspDispatcher.register(new DidChangeHandler(), "textDocument/didChange"); + lspDispatcher.register(new DidSaveHandler(), "textDocument/didSave"); + lspDispatcher.register(new DefinitionHandler(), "textDocument/definition"); + lspDispatcher.register(new DocumentSymbolHandler(), "textDocument/documentSymbol"); + lspDispatcher.register(new CompletionHandler(), "textDocument/completion"); + lspDispatcher.register(new CodeLensHandler(), "textDocument/codeLens", "codeLens/resolve"); + lspDispatcher.register(new ReferencesHandler(), "textDocument/references"); + lspDispatcher.register(new TypeHierarchyHandler(), "textDocument/prepareTypeHierarchy", "typeHierarchy/supertypes", "typeHierarchy/subtypes"); + + lspDispatcher.register(new DidChangeWSHandler(), "workspace/didChangeWatchedFiles"); + + lspDispatcher.register(new UnknownHandler()); // Called for unknown methods + } + public static void reset() { Diag.config("Resetting WorkspaceManagers, PluginRegistry, EventHub and MessageHub"); - LSPXWorkspaceManager.reset(); - DAPWorkspaceManager.reset(); - DAPXWorkspaceManager.reset(); + DAPPlugin.reset(); PluginRegistry.reset(); EventHub.reset(); MessageHub.reset(); @@ -206,7 +264,7 @@ public RPCMessageList lspInitialize(RPCRequest request, JSONObject clientInfo, F this.clientCapabilities = clientCapabilities; this.openFiles.clear(); - LSPXWorkspaceManager.getInstance().enablePlugins(); + enablePlugins(); System.setProperty("vdmj.parser.tabstop", "1"); // Forced, for LSP location offsets Diag.info("Reading properties from %s", PROPERTIES); @@ -235,6 +293,97 @@ public RPCMessageList lspInitialized(RPCRequest request) } } + /** + * This is called after the client capabilities have been received. If the option + * is enabled in the capabilities, the relevant plugin is registered. + * + * PO and CT are built-in, but still enabled by the capabilities. + * + * Further plugins may be loaded via the property/resource "lspx.plugins". + */ + private void enablePlugins() throws Exception + { + if (hasClientCapability("experimental.proofObligationGeneration")) + { + registry.registerPlugin(POPlugin.factory(Settings.dialect)); + } + + if (hasClientCapability("experimental.combinatorialTesting")) + { + registry.registerPlugin(CTPlugin.factory(Settings.dialect)); + } + + List plugins = GetResource.readResource("lspx.plugins"); + + if (!plugins.isEmpty()) + { + for (String plugin: plugins) + { + try + { + Class clazz = Class.forName(plugin); + + try + { + Method factory = clazz.getMethod("factory", Dialect.class); + AnalysisPlugin instance = (AnalysisPlugin)factory.invoke(null, Settings.dialect); + registry.registerPlugin(instance); + Diag.info("Registered LSPX plugin %s", plugin); + } + catch (NoSuchMethodException e) // Try default constructor + { + try + { + if (Modifier.isAbstract(clazz.getModifiers())) + { + Diag.severe("Plugin class is abstract: %s", clazz.getName()); + continue; + } + + Constructor ctor = clazz.getConstructor(); + AnalysisPlugin instance = (AnalysisPlugin) ctor.newInstance(); + registry.registerPlugin(instance); + Diag.info("Registered LSPX plugin %s", plugin); + } + catch (Throwable th) + { + Diag.error(th); + Diag.error("Cannot register LSPX plugin %s", plugin); + } + } + catch (Exception e) + { + Diag.error(e); + Diag.error("Plugin %s factory method failed", plugin); + } + } + catch (ClassNotFoundException e) + { + Diag.error("Plugin class %s not found", plugin); + } + } + } + else + { + Diag.info("No external plugins configured in lspx.plugins"); + } + } + + public RPCMessageList unhandledMethod(RPCRequest request) + { + RPCMessageList results = eventhub.publish(new UnknownMethodEvent(request)); + + if (results.isEmpty()) + { + Diag.error("No external plugin registered for " + request.getMethod()); + return new RPCMessageList(request, RPCErrors.MethodNotFound, request.getMethod()); + } + else + { + return results; + } + } + public boolean hasClientCapability(String dotName) // eg. "workspace.workspaceFolders" { Object cap = getClientCapability(dotName); @@ -1306,7 +1455,7 @@ else if (def.location.file.getName().equals("console") || else if (def instanceof TCClassDefinition) { TCClassDefinition cdef = (TCClassDefinition)def; - return new RPCMessageList(request, msgutils.typeHierarchyItem(cdef)); + return new RPCMessageList(request, messages.typeHierarchyItem(cdef)); } else { @@ -1319,14 +1468,14 @@ public RPCMessageList lspSupertypes(RPCRequest request, String classname) { TCPlugin tc = registry.getPlugin("TC"); TCClassList results = tc.getTypeHierarchy(classname, false); - return new RPCMessageList(request, msgutils.typeHierarchyItems(results)); + return new RPCMessageList(request, messages.typeHierarchyItems(results)); } public RPCMessageList lspSubtypes(RPCRequest request, String classname) { TCPlugin tc = registry.getPlugin("TC"); TCClassList results = tc.getTypeHierarchy(classname, true); - return new RPCMessageList(request, msgutils.typeHierarchyItems(results)); + return new RPCMessageList(request, messages.typeHierarchyItems(results)); } public RPCMessageList lspCompletion(RPCRequest request, diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 53eb124fb..939bf1207 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -34,6 +34,8 @@ import json.JSONArray; import json.JSONObject; import lsp.Utils; +import lsp.lspx.POGHandler; +import rpc.RPCErrors; import rpc.RPCMessageList; import rpc.RPCRequest; import workspace.Diag; @@ -82,6 +84,8 @@ public int getPriority() @Override public void init() { + lspDispatcher.register(new POGHandler(), "slsp/POG/generate"); + eventhub.register(CheckPrepareEvent.class, this); eventhub.register(CheckCompleteEvent.class, this); } @@ -153,6 +157,24 @@ protected JSONArray splitPO(String value) return array; } + public RPCMessageList pogGenerate(RPCRequest request, File file) + { + try + { + if (messagehub.hasErrors()) // No clean tree + { + return new RPCMessageList(request, RPCErrors.InvalidRequest, "Specification errors found"); + } + + return getJSONObligations(request, file); + } + catch (Exception e) + { + Diag.error(e); + return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); + } + } + public RPCMessageList getJSONObligations(RPCRequest request, File file) { JSONArray poList = new JSONArray(); diff --git a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java b/lsp/src/main/java/workspace/plugins/TRPlugin.java similarity index 51% rename from lsp/src/main/java/workspace/LSPXWorkspaceManager.java rename to lsp/src/main/java/workspace/plugins/TRPlugin.java index cb121980d..d238bd0b7 100644 --- a/lsp/src/main/java/workspace/LSPXWorkspaceManager.java +++ b/lsp/src/main/java/workspace/plugins/TRPlugin.java @@ -1,6 +1,6 @@ /******************************************************************************* * - * Copyright (c) 2020 Nick Battle. + * Copyright (c) 2023 Nick Battle. * * Author: Nick Battle * @@ -22,317 +22,64 @@ * ******************************************************************************/ -package workspace; +package workspace.plugins; import java.io.File; import java.io.FileOutputStream; import java.io.IOException; import java.io.PrintWriter; -import java.lang.reflect.Constructor; -import java.lang.reflect.Method; -import java.lang.reflect.Modifier; import java.nio.file.Path; import java.nio.file.Paths; -import java.util.List; import java.util.Map; import java.util.Set; -import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.runtime.SourceFile; -import com.fujitsu.vdmj.tc.lex.TCNameList; -import com.fujitsu.vdmj.tc.lex.TCNameToken; -import com.fujitsu.vdmj.traces.TraceReductionType; -import com.fujitsu.vdmj.util.GetResource; -import json.JSONArray; import json.JSONObject; -import lsp.LSPException; -import lsp.Utils; +import lsp.lspx.TranslateHandler; import rpc.RPCErrors; import rpc.RPCMessageList; import rpc.RPCRequest; -import workspace.events.UnknownMethodEvent; -import workspace.plugins.AnalysisPlugin; -import workspace.plugins.CTPlugin; -import workspace.plugins.POPlugin; -import workspace.plugins.TCPlugin; +import workspace.EventListener; -public class LSPXWorkspaceManager +/** + * The translate plugin. + */ +public class TRPlugin extends AnalysisPlugin implements EventListener { - private static LSPXWorkspaceManager INSTANCE = null; - private final PluginRegistry registry; - private final EventHub eventhub; - private final MessageHub messagehub; - private final LSPWorkspaceManager wsManager; + private final LSPPlugin lspPlugin; - protected LSPXWorkspaceManager() + public static AnalysisPlugin factory(Dialect dialect) { - this.registry = PluginRegistry.getInstance(); - this.eventhub = EventHub.getInstance(); - this.messagehub = MessageHub.getInstance(); - this.wsManager = LSPWorkspaceManager.getInstance(); - } - - public static synchronized LSPXWorkspaceManager getInstance() - { - if (INSTANCE == null) - { - INSTANCE = new LSPXWorkspaceManager(); - Diag.info("Created LSPXWorkspaceManager"); - } - - return INSTANCE; - } - - /** - * This is called after the client capabilities have been received. If the option - * is enabled in the capabilities, the relevant plugin is registered. - * - * PO and CT are built-in, but still enabled by the capabilities. - * - * Further plugins may be loaded via the property "lspx.plugins". - * @throws Exception - */ - public void enablePlugins() throws Exception - { - if (wsManager.hasClientCapability("experimental.proofObligationGeneration")) - { - registry.registerPlugin(POPlugin.factory(Settings.dialect)); - } - - if (wsManager.hasClientCapability("experimental.combinatorialTesting")) - { - registry.registerPlugin(CTPlugin.factory(Settings.dialect)); - } - - List plugins = GetResource.readResource("lspx.plugins"); - - if (!plugins.isEmpty()) - { - for (String plugin: plugins) - { - try - { - Class clazz = Class.forName(plugin); - - try - { - Method factory = clazz.getMethod("factory", Dialect.class); - AnalysisPlugin instance = (AnalysisPlugin)factory.invoke(null, Settings.dialect); - registry.registerPlugin(instance); - Diag.info("Registered LSPX plugin %s", plugin); - } - catch (NoSuchMethodException e) // Try default constructor - { - try - { - if (Modifier.isAbstract(clazz.getModifiers())) - { - Diag.severe("Plugin class is abstract: %s", clazz.getName()); - continue; - } - - Constructor ctor = clazz.getConstructor(); - AnalysisPlugin instance = (AnalysisPlugin) ctor.newInstance(); - registry.registerPlugin(instance); - Diag.info("Registered LSPX plugin %s", plugin); - } - catch (Throwable th) - { - Diag.error(th); - Diag.error("Cannot register LSPX plugin %s", plugin); - } - } - catch (Exception e) - { - Diag.error(e); - Diag.error("Plugin %s factory method failed", plugin); - } - } - catch (ClassNotFoundException e) - { - Diag.error("Plugin class %s not found", plugin); - } - } - } - else - { - Diag.info("No external plugins configured in lspx.plugins"); - } - } - - public RPCMessageList unhandledMethod(RPCRequest request) - { - RPCMessageList results = eventhub.publish(new UnknownMethodEvent(request)); - - if (results.isEmpty()) - { - Diag.error("No external plugin registered for " + request.getMethod()); - return new RPCMessageList(request, RPCErrors.MethodNotFound, request.getMethod()); - } - else + switch (dialect) { - return results; - } - } - - /** - * Reset the singleton. - */ - public static void reset() - { - if (INSTANCE != null) - { - INSTANCE = null; + default: + return new TRPlugin(); } } - /** - * LSPX extensions... - */ - - public RPCMessageList pogGenerate(RPCRequest request, File file) + private TRPlugin() { - try - { - if (messagehub.hasErrors()) // No clean tree - { - return new RPCMessageList(request, RPCErrors.InvalidRequest, "Specification errors found"); - } - - POPlugin po = registry.getPlugin("PO"); - return po.getJSONObligations(request, file); - } - catch (Exception e) - { - Diag.error(e); - return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); - } + lspPlugin = LSPPlugin.getInstance(); } - - public RPCMessageList ctTraces(RPCRequest request, File project) + + @Override + public int getPriority() { - try - { - if (specHasErrors()) - { - return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); - } - - DAPWorkspaceManager.getInstance().refreshInterpreter(); - CTPlugin ct = registry.getPlugin("CT"); - Map nameMap = ct.getTraceNames(); - JSONArray results = new JSONArray(); - - for (String module: nameMap.keySet()) - { - JSONArray array = new JSONArray(); - - for (TCNameToken name: nameMap.get(module)) - { - array.add(new JSONObject( - "name", name.getExplicit(true).toString(), - "location", Utils.lexLocationToLocation(name.getLocation()))); - } - - results.add(new JSONObject("name", module, "traces", array)); - } - - return new RPCMessageList(request, results); - } - catch (Exception e) - { - Diag.error(e); - return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); - } + return EventListener.TR_PRIORITY; } - public RPCMessageList ctGenerate(RPCRequest request, String name) + @Override + public String getName() { - try - { - if (specHasErrors()) - { - return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); - } - - CTPlugin ct = registry.getPlugin("CT"); - - if (ct.isRunning()) - { - return new RPCMessageList(request, RPCErrors.InvalidRequest, "Trace still running"); - } - - DAPWorkspaceManager.getInstance().refreshInterpreter(); - TCNameToken tracename = Utils.stringToName(name); - int count = ct.generate(tracename); - return new RPCMessageList(request, new JSONObject("numberOfTests", count)); - } - catch (LSPException e) - { - Diag.error(e); - return new RPCMessageList(request, e.getError(), e.getMessage()); - } - catch (Exception e) - { - Diag.error(e); - return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); - } + return "TR"; } - public RPCMessageList ctExecute(RPCRequest request, String name, - Object progressToken, Object workDoneToken, - TraceReductionType rType, float subset, long seed, Long start, Long end) - { - try - { - if (specHasErrors()) - { - return new RPCMessageList(request, RPCErrors.ParseError, "Specification has errors"); - } - - TCNameToken tracename = Utils.stringToName(name); - CTPlugin ct = registry.getPlugin("CT"); - - if (ct.isRunning()) - { - return new RPCMessageList(request, RPCErrors.InvalidRequest, "Trace still running"); - } - - if (DAPWorkspaceManager.getInstance().refreshInterpreter()) - { - Diag.error("The spec has changed since generate, so re-generating"); - ct.generate(tracename); - } - - JSONArray batch = ct.runTraceRange(request, tracename, progressToken, workDoneToken, - rType, subset, seed, start, end); - - if (batch == null) // Running in background - { - return null; - } - else - { - return new RPCMessageList(request, batch); - } - } - catch (LSPException e) - { - Diag.error(e); - return new RPCMessageList(request, e.getError(), e.getMessage()); - } - catch (Exception e) - { - Diag.error(e); - return new RPCMessageList(request, RPCErrors.InternalError, e.getMessage()); - } - } - - private boolean specHasErrors() + @Override + public void init() { - return messagehub.hasErrors(); + lspDispatcher.register(new TranslateHandler(), "slsp/TR/translate"); } /** @@ -340,7 +87,7 @@ private boolean specHasErrors() */ private File getSubFolder(File saveUri, File file) { - File root = wsManager.getRoot(); + File root = lspPlugin.getRoot(); if (file.getParent().startsWith(root.getPath())) { @@ -356,7 +103,7 @@ private File getSubFolder(File saveUri, File file) public RPCMessageList translateLaTeX(RPCRequest request, File file, File saveUri, JSONObject options) { File responseFile = null; - Map filemap = wsManager.getProjectFiles(); + Map filemap = lspPlugin.getProjectFiles(); try { @@ -383,7 +130,7 @@ else if (file.isDirectory()) } } - if (file.equals(wsManager.getRoot())) + if (file.equals(lspPlugin.getRoot())) { createLaTeXDocument(saveUri, filemap.keySet()); } @@ -409,7 +156,7 @@ else if (filemap.containsKey(file)) private void createLaTeXDocument(File saveUri, Set sources) throws IOException { - String project = wsManager.getRoot().getName(); + String project = lspPlugin.getRoot().getName(); File document = new File(saveUri, project + ".tex"); PrintWriter out = new PrintWriter(new FileOutputStream(document)); @@ -425,7 +172,7 @@ private void createLaTeXDocument(File saveUri, Set sources) throws IOExcep out.println("\\tableofcontents"); out.println(); - Path sourceBase = Paths.get(wsManager.getRoot().getAbsolutePath()); + Path sourceBase = Paths.get(lspPlugin.getRoot().getAbsolutePath()); for (File pfile: sources) { @@ -485,7 +232,7 @@ private File fileToLaTeX(File saveUri, File file, JSONObject options) throws IOE public RPCMessageList translateWord(RPCRequest request, File file, File saveUri, JSONObject options) { File responseFile = null; - Map filemap = wsManager.getProjectFiles(); + Map filemap = lspPlugin.getProjectFiles(); try { @@ -547,7 +294,7 @@ private File fileToWord(File saveUri, File file) throws IOException public RPCMessageList translateCoverage(RPCRequest request, File file, File saveUri, JSONObject options) { File responseFile = null; - Map filemap = wsManager.getProjectFiles(); + Map filemap = lspPlugin.getProjectFiles(); try { diff --git a/lsp/src/test/java/lsp/DAPTest.java b/lsp/src/test/java/lsp/DAPTest.java index 36c07c2e1..a75dd44ed 100644 --- a/lsp/src/test/java/lsp/DAPTest.java +++ b/lsp/src/test/java/lsp/DAPTest.java @@ -37,18 +37,14 @@ import json.JSONWriter; import rpc.RPCMessageList; import rpc.RPCRequest; -import workspace.DAPWorkspaceManager; -import workspace.DAPXWorkspaceManager; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.DAPPlugin; +import workspace.plugins.LSPPlugin; abstract public class DAPTest { - protected LSPWorkspaceManager lspManager = null; - protected LSPXWorkspaceManager lspxManager = null; - protected DAPWorkspaceManager dapManager = null; - protected DAPXWorkspaceManager dapxManager = null; + protected LSPPlugin lspManager = null; + protected DAPPlugin dapManager = null; static { @@ -58,11 +54,9 @@ abstract public class DAPTest protected void setupWorkspace(Dialect dialect) throws IOException { Settings.dialect = dialect; - LSPWorkspaceManager.reset(); // Clears other managers, registry and hubs too - lspManager = LSPWorkspaceManager.getInstance(); - lspxManager = LSPXWorkspaceManager.getInstance(); - dapManager = DAPWorkspaceManager.getInstance(); - dapxManager = DAPXWorkspaceManager.getInstance(); + LSPPlugin.reset(); // Clears other managers, registry and hubs too + lspManager = LSPPlugin.getInstance(); + dapManager = DAPPlugin.getInstance(); } protected RPCMessageList initialize(File root, JSONObject capabilities) throws Exception diff --git a/lsp/src/test/java/lsp/LSPTest.java b/lsp/src/test/java/lsp/LSPTest.java index 74acd172f..681ecb2cd 100644 --- a/lsp/src/test/java/lsp/LSPTest.java +++ b/lsp/src/test/java/lsp/LSPTest.java @@ -37,18 +37,14 @@ import json.JSONWriter; import rpc.RPCMessageList; import rpc.RPCRequest; -import workspace.DAPWorkspaceManager; -import workspace.DAPXWorkspaceManager; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.DAPPlugin; +import workspace.plugins.LSPPlugin; abstract public class LSPTest { - protected LSPWorkspaceManager lspManager = null; - protected LSPXWorkspaceManager lspxManager = null; - protected DAPWorkspaceManager dapManager = null; - protected DAPXWorkspaceManager dapxManager = null; + protected LSPPlugin lspManager = null; + protected DAPPlugin dapManager = null; static { @@ -58,11 +54,9 @@ abstract public class LSPTest protected void setupWorkspace(Dialect dialect) throws IOException { Settings.dialect = dialect; - LSPWorkspaceManager.reset(); // resets other managers, registry and hubs - lspManager = LSPWorkspaceManager.getInstance(); - lspxManager = LSPXWorkspaceManager.getInstance(); - dapManager = DAPWorkspaceManager.getInstance(); - dapxManager = DAPXWorkspaceManager.getInstance(); + LSPPlugin.reset(); // resets other managers, registry and hubs + lspManager = LSPPlugin.getInstance(); + dapManager = DAPPlugin.getInstance(); } protected RPCMessageList initialize(File root, JSONObject capabilities) throws Exception diff --git a/pom.xml b/pom.xml index 423189a12..660c44404 100644 --- a/pom.xml +++ b/pom.xml @@ -66,7 +66,7 @@ maven-compiler-plugin 3.11.0 - 8 + 11 diff --git a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index ffa76d1cf..ba7e7990d 100644 --- a/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -47,10 +47,10 @@ import rpc.RPCMessageList; import rpc.RPCRequest; import vdmj.commands.AnalysisCommand; -import workspace.DAPWorkspaceManager; import workspace.Diag; import workspace.PluginRegistry; import workspace.plugins.AnalysisPlugin; +import workspace.plugins.DAPPlugin; import workspace.plugins.POPlugin; public class QuickCheckLSPPlugin extends AnalysisPlugin @@ -87,7 +87,7 @@ else if (CancellableThread.currentlyRunning() != null) return new RPCMessageList(request, RPCErrors.InternalError, "Running " + CancellableThread.currentlyRunning()); } - DAPWorkspaceManager manager = DAPWorkspaceManager.getInstance(); + DAPPlugin manager = DAPPlugin.getInstance(); Interpreter interpreter = manager.getInterpreter(); if (interpreter.getInitialContext() == null) // eg. from unit tests diff --git a/quickcheck/src/main/resources/META-INF/plugin.json b/quickcheck/src/main/resources/META-INF/plugin.json new file mode 100644 index 000000000..1dc6b8579 --- /dev/null +++ b/quickcheck/src/main/resources/META-INF/plugin.json @@ -0,0 +1,6 @@ +{ + "name": "quickcheck", + "description": "QuickCheck lightweight verification plugin", + "dialects": [ "vdmsl", "vdmpp", "vdmrt" ], + "precision": "standard" +} diff --git a/quickcheck/src/test/java/tests/LSPTest.java b/quickcheck/src/test/java/tests/LSPTest.java index d0084b400..b9423400f 100644 --- a/quickcheck/src/test/java/tests/LSPTest.java +++ b/quickcheck/src/test/java/tests/LSPTest.java @@ -37,18 +37,14 @@ import json.JSONWriter; import rpc.RPCMessageList; import rpc.RPCRequest; -import workspace.DAPWorkspaceManager; -import workspace.DAPXWorkspaceManager; import workspace.Diag; -import workspace.LSPWorkspaceManager; -import workspace.LSPXWorkspaceManager; +import workspace.plugins.DAPPlugin; +import workspace.plugins.LSPPlugin; abstract public class LSPTest { - protected LSPWorkspaceManager lspManager = null; - protected LSPXWorkspaceManager lspxManager = null; - protected DAPWorkspaceManager dapManager = null; - protected DAPXWorkspaceManager dapxManager = null; + protected LSPPlugin lspManager = null; + protected DAPPlugin dapManager = null; static { @@ -58,11 +54,9 @@ abstract public class LSPTest protected void setupWorkspace(Dialect dialect) throws IOException { Settings.dialect = dialect; - LSPWorkspaceManager.reset(); // resets other managers, registry and hubs - lspManager = LSPWorkspaceManager.getInstance(); - lspxManager = LSPXWorkspaceManager.getInstance(); - dapManager = DAPWorkspaceManager.getInstance(); - dapxManager = DAPXWorkspaceManager.getInstance(); + LSPPlugin.reset(); // resets other managers, registry and hubs + lspManager = LSPPlugin.getInstance(); + dapManager = DAPPlugin.getInstance(); } protected RPCMessageList initialize(File root, JSONObject capabilities) throws Exception diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleDebugLink.java b/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleDebugLink.java index c3fab3a89..d4c4647f6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleDebugLink.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/debug/ConsoleDebugLink.java @@ -30,6 +30,7 @@ import java.util.Map; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Breakpoint; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; @@ -392,7 +393,7 @@ public void breakpoint(Context ctxt, Breakpoint bp) if (thread.getSignal() == Signal.TERMINATE) { - throw new ThreadDeath(); // Just die, as we're not continuing. + throw new VDMThreadDeath(); // Just die, as we're not continuing. } } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/messages/VDMThreadDeath.java b/vdmj/src/main/java/com/fujitsu/vdmj/messages/VDMThreadDeath.java new file mode 100644 index 000000000..39bf1a299 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/messages/VDMThreadDeath.java @@ -0,0 +1,32 @@ +/******************************************************************************* + * + * Copyright (c) 2023 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package com.fujitsu.vdmj.messages; + +/** + * A replacement for the deprecated java.lang.ThreadDeath. + */ +public class VDMThreadDeath extends Error +{ + private static final long serialVersionUID = 1L; +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/AsyncThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/AsyncThread.java index 344358ad7..82f9cd212 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/AsyncThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/AsyncThread.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.debug.DebugLink; import com.fujitsu.vdmj.debug.DebugReason; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.ClassInterpreter; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; @@ -121,10 +122,9 @@ protected void body() ResourceScheduler.setException(e); SchedulableThread.signalAll(Signal.SUSPEND); } - catch (ThreadDeath e) + catch (VDMThreadDeath e) { completeReason = DebugReason.ABORTED; - throw e; } catch (Throwable th) // Java errors not caught above { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/BusThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/BusThread.java index e712b7423..e0ec636db 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/BusThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/BusThread.java @@ -25,6 +25,7 @@ package com.fujitsu.vdmj.scheduler; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Context; public class BusThread extends SchedulableThread @@ -52,7 +53,7 @@ protected void handleSignal(Signal sig, Context ctxt, LexLocation location) switch (sig) { case TERMINATE: - throw new ThreadDeath(); + throw new VDMThreadDeath(); case SUSPEND: // Ignore break; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/InitThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/InitThread.java index 55b5cd4e9..dac060180 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/InitThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/InitThread.java @@ -37,6 +37,7 @@ import com.fujitsu.vdmj.in.modules.INModuleList; import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.messages.Console; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Breakpoint; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; @@ -128,7 +129,7 @@ else if (classes != null) setException(e); suspendOthers(); } - catch (ThreadDeath th) + catch (VDMThreadDeath th) { // Fine } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/MainThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/MainThread.java index 2a6b52eac..ff62349db 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/MainThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/MainThread.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.debug.DebugLink; import com.fujitsu.vdmj.debug.DebugReason; import com.fujitsu.vdmj.in.expressions.INExpression; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Breakpoint; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; @@ -94,10 +95,9 @@ public void body() setException(e); suspendOthers(); } - catch (ThreadDeath e) + catch (VDMThreadDeath e) { completeReason = DebugReason.ABORTED; - throw e; } catch (Throwable th) // Java errors not caught above { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/ObjectThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/ObjectThread.java index f41e886aa..c9da9a98d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/ObjectThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/ObjectThread.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.debug.DebugLink; import com.fujitsu.vdmj.debug.DebugReason; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; import com.fujitsu.vdmj.runtime.ObjectContext; @@ -113,10 +114,9 @@ public void body() ResourceScheduler.setException(e); SchedulableThread.signalAll(Signal.SUSPEND); } - catch (ThreadDeath e) + catch (VDMThreadDeath e) { completeReason = DebugReason.ABORTED; - throw e; } catch (Throwable th) // Java errors not caught above { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/PeriodicThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/PeriodicThread.java index 10352e0c0..3ad1dbe2c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/PeriodicThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/PeriodicThread.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.debug.DebugLink; import com.fujitsu.vdmj.debug.DebugReason; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.ClassInterpreter; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; @@ -170,10 +171,9 @@ protected void body() ResourceScheduler.setException(e); SchedulableThread.signalAll(Signal.SUSPEND); } - catch (ThreadDeath e) + catch (VDMThreadDeath e) { completeReason = DebugReason.ABORTED; - throw e; } catch (Throwable th) // Java errors not caught above { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/SchedulableThread.java b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/SchedulableThread.java index 024ff2399..50de38677 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/SchedulableThread.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/scheduler/SchedulableThread.java @@ -38,6 +38,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.messages.InternalException; import com.fujitsu.vdmj.messages.RTLogger; +import com.fujitsu.vdmj.messages.VDMThreadDeath; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.ContextException; import com.fujitsu.vdmj.runtime.ExceptionHandler; @@ -153,6 +154,10 @@ public void run() reschedule(null, null); body(); } + catch (VDMThreadDeath e) + { + // Exit cleanly + } finally { setState(RunState.COMPLETE); @@ -308,7 +313,7 @@ private void sleep(Context ctxt, LexLocation location) if (stopCalled && state == RunState.RUNNING) { // stopThread made us RUNNABLE, now we're running, so die - throw new ThreadDeath(); + throw new VDMThreadDeath(); } return; @@ -331,7 +336,7 @@ protected void handleSignal(Signal sig, Context ctxt, LexLocation location) switch (sig) { case TERMINATE: - throw new ThreadDeath(); + throw new VDMThreadDeath(); case SUSPEND: DebugLink.getInstance().stopped(ctxt, location, null); @@ -339,7 +344,7 @@ protected void handleSignal(Signal sig, Context ctxt, LexLocation location) case DEADLOCKED: DebugLink.getInstance().stopped(ctxt, location, new Exception("DEADLOCK detected")); - throw new ThreadDeath(); + throw new VDMThreadDeath(); } }