Added interface for plugins to add JsonRpcRequestHandlers to the language server

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -110,7 +110,7 @@ private Action<LanguageServerOptions> GetServerOptionsAction(Action<DafnyOptions
       LanguageServer.ConfigureDafnyOptionsForServer(dafnyOptions);
       ApplyDefaultOptionValues(dafnyOptions);
       return options => {
-        options.WithDafnyLanguageServer(() => { });
+        options.WithDafnyLanguageServer(dafnyOptions, () => { });
         options.Services.AddSingleton(dafnyOptions);
         options.Services.AddSingleton<IProgramVerifier>(serviceProvider => new SlowVerifier(
           serviceProvider.GetRequiredService<ILogger<DafnyProgramVerifier>>()

Source/DafnyLanguageServer.Test/Various/PluginsHandlerTest.cs

@@ -0,0 +1,30 @@
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Xunit.Abstractions;
+using Xunit;
+using System.Threading;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various;
+
+public class PluginsHandlerTest : PluginsTestBase {
+
+  protected override string LibraryName =>
+    "PluginsHandlerTest";
+
+  protected override string[] CommandLineArgument =>
+    new[] { $"{LibraryPath}" };
+
+  [Fact]
+  public async Task EnsureWithPluginHandlersWorks() {
+    var documentItem = CreateTestDocument(@"
+method firstMethod() {
+}");
+    var cancellationToken = new CancellationToken();
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var requestResult = await client.SendRequest("dafny/request/dummy").Returning<string>(cancellationToken);
+    Assert.Equal("dummy", requestResult);
+  }
+
+  public PluginsHandlerTest(ITestOutputHelper output) : base(output) {
+  }
+}

Source/DafnyLanguageServer.Test/Various/PluginsTestBase.cs

@@ -38,13 +38,15 @@ private static string GetLibrary(string assemblyName) {
       "DafnyCore",
       "System",
       "netstandard",
+      "OmniSharp.Extensions.JsonRpc",
       "OmniSharp.Extensions.LanguageServer",
       "OmniSharp.Extensions.LanguageProtocol",
       "System.Console",
       "DafnyLanguageServer",
       "System.Runtime",
       "Boogie.Core",
-      "System.Collections"
+      "System.Collections",
+      "MediatR"
     };
     compilation = compilation.AddReferences(standardLibraries.Select(fileName =>
         MetadataReference.CreateFromFile(Assembly.Load((string)fileName).Location)))
@@ -53,7 +55,7 @@ private static string GetLibrary(string assemblyName) {
       .WithOptions(
         new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary)
       );
-    var syntaxTree = CSharpSyntaxTree.ParseText(code);
+    var syntaxTree = CSharpSyntaxTree.ParseText(code, CSharpParseOptions.Default.WithLanguageVersion(LanguageVersion.CSharp9));
     compilation = compilation.AddSyntaxTrees(syntaxTree);
     var assemblyPath = $"{temp}.dll";
     var result = compilation.Emit(assemblyPath);

Source/DafnyLanguageServer.Test/_plugins/PluginsHandlerTest.cs

@@ -0,0 +1,26 @@
+using OmniSharp.Extensions.LanguageServer.Server;
+using MediatR;
+using OmniSharp.Extensions.JsonRpc;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace PluginsHandlerTest {
+  /// <summary>
+  ///  Small plugin that adds a request to the language server, which simply returns a dummy string
+  /// </summary>
+  public class TestConfiguration : Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration {
+    public override LanguageServerOptions WithPluginHandlers(LanguageServerOptions options) {
+      return options.WithHandler<DummyHandler>();
+    }
+  }
+
+  [Parallel]
+  [Method("dafny/request/dummy", Direction.ClientToServer)]
+  public record DummyParams : IRequest<string>;
+
+  public class DummyHandler : IJsonRpcRequestHandler<DummyParams, string> {
+    public async Task<string> Handle(DummyParams request, CancellationToken cancellationToken) {
+      return "dummy";
+    }
+  }
+}

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -23,15 +23,15 @@ private static string DafnyVersion {
       }
     }
 
-    public static LanguageServerOptions WithDafnyLanguageServer(this LanguageServerOptions options, Action killLanguageServer) {
+    public static LanguageServerOptions WithDafnyLanguageServer(this LanguageServerOptions options, DafnyOptions dafnyOptions, Action killLanguageServer) {
       options.ServerInfo = new ServerInfo {
         Name = "Dafny",
         Version = DafnyVersion
       };
       return options
         .WithDafnyLanguage()
         .WithDafnyWorkspace()
-        .WithDafnyHandlers()
+        .WithDafnyHandlers(dafnyOptions)
         .OnInitialize((server, @params, token) => InitializeAsync(server, @params, token, killLanguageServer))
         .OnStarted(StartedAsync);
     }

Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs

@@ -1,6 +1,7 @@
 using Microsoft.Dafny.LanguageServer.Handlers.Custom;
-using OmniSharp.Extensions.JsonRpc;
+using Microsoft.Dafny.LanguageServer.Plugins;
 using OmniSharp.Extensions.LanguageServer.Server;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny.LanguageServer.Handlers {
   /// <summary>
@@ -12,7 +13,11 @@ public static class LanguageServerExtensions {
     /// </summary>
     /// <param name="options">The language server where the handlers should be registered to.</param>
     /// <returns>The language server enriched with the dafny handlers.</returns>
-    public static LanguageServerOptions WithDafnyHandlers(this LanguageServerOptions options) {
+    public static LanguageServerOptions WithDafnyHandlers(this LanguageServerOptions options, DafnyOptions dafnyOptions) {
+      foreach (var plugin in dafnyOptions.Plugins) {
+        options = plugin is ConfiguredPlugin { Configuration: PluginConfiguration configuration } ?
+          configuration.WithPluginHandlers(options) : options;
+      }
       return options
         .WithHandler<DafnyTextDocumentHandler>()
         .WithHandler<DafnyDocumentSymbolHandler>()

Source/DafnyLanguageServer/LanguageServer.cs

@@ -65,7 +65,7 @@ public static async Task Start(DafnyOptions dafnyOptions) {
             .ConfigureLogging(SetupLogging)
             .WithUnhandledExceptionHandler(LogException)
             // ReSharper disable once AccessToModifiedClosure
-            .WithDafnyLanguageServer(() => shutdownServer!())
+            .WithDafnyLanguageServer(dafnyOptions, () => shutdownServer!())
         );
         // Prevent any other parts of the language server to actually write to standard output.
         await using var logWriter = new LogWriter();

Source/DafnyLanguageServer/Plugins/PluginConfiguration.cs

@@ -1,5 +1,6 @@
 // SPDX-License-Identifier: MIT
 using System;
+using OmniSharp.Extensions.LanguageServer.Server;
 
 namespace Microsoft.Dafny.LanguageServer.Plugins;
 
@@ -21,4 +22,12 @@ public abstract class PluginConfiguration : Dafny.Plugins.PluginConfiguration {
   public virtual DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
     return Array.Empty<DafnyCodeActionProvider>();
   }
+
+  /// <summary>
+  /// Override this method to provide additional language server handlers
+  /// </summary>
+  /// <returns>The provided LanguageServerOptions with the additional handlers applied</returns>
+  public virtual LanguageServerOptions WithPluginHandlers(LanguageServerOptions options) {
+    return options;
+  }
 }

docs/DafnyRef/Plugins.md

@@ -6,18 +6,19 @@ without concern for verifying or compiling the program. Or it might modify the p
 and then continue on with verification and compilation with the core Dafny tool. A user plugin might also be used
 in the Language Server and thereby be available in the VSCode (or other) IDE.
 
-_ **This is an experimental aspect of Dafny.**
+_**This is an experimental aspect of Dafny.**
 The plugin API directly exposes the Dafny AST, which is constantly evolving.
 Hence, always recompile your plugin against the binary of Dafny that will be importing your plugin._
 
-Plugins are libraries linked to a `Dafny.dll` of the same version as the language server.
+Plugins are libraries linked to a `Dafny.dll` of the same version as the Language Server.
 A plugin typically defines:
 
 * Zero or one class extending `Microsoft.Dafny.Plugins.PluginConfiguration`, which receives plugins arguments in its method `ParseArguments`, and
-  1) Can return a list of `Microsoft.Dafny.Plugins.Rewriter`s when its method `GetRewriters()` is called by Dafny,
-  2) Can return a list of `Microsoft.Dafny.Plugins.Compiler`s when its method `GetCompilers()` is called by Dafny,
-  3) If the configuration extends the subclass `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration`,
-     then it can return a list of `Microsoft.Dafny.LanguageServer.Plugins.DafnyCodeActionProvider`s when its method `GetDafnyCodeActionProviders()` is called by the Dafny Language Server.
+  1. Can return a list of `Microsoft.Dafny.Plugins.Rewriter`s when its method `GetRewriters()` is called by Dafny,
+  2. Can return a list of `Microsoft.Dafny.Plugins.Compiler`s when its method `GetCompilers()` is called by Dafny,
+  3. If the configuration extends the subclass `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration`:
+      1. Can return a list of `Microsoft.Dafny.LanguageServer.Plugins.DafnyCodeActionProvider`s when its method `GetDafnyCodeActionProviders()` is called by the Dafny Language Server.
+      2. Can return a modified version of `OmniSharp.Extensions.LanguageServer.Server.LanguageServerOptions` when its method `WithPluginHandlers()` is called by the Dafny Language Server.
 
 * Zero or more classes extending `Microsoft.Dafny.Plugins.Rewriter`.
   If a configuration class is provided, it is responsible for instantiating them and returning them in `GetRewriters()`.
@@ -29,6 +30,7 @@ A plugin typically defines:
   Only a configuration class of type `Microsoft.Dafny.LanguageServer.Plugins.PluginConfiguration` can be responsible for instantiating them and returning them in `GetDafnyCodeActionProviders()`.
 
 The most important methods of the class `Rewriter` that plugins override are
+
 * (experimental) `PreResolve(ModuleDefinition)`: Here you can optionally modify the AST before it is resolved.
 * `PostResolve(ModuleDefinition)`: This method is repeatedly called with every resolved and type-checked module, before verification.
   Plugins override this method typically to report additional diagnostics.
@@ -38,11 +40,12 @@ Plugins are typically used to report additional diagnostics such as unsupported
 
 Note that all plugin errors should use the original program's expressions' token and NOT `Token.NoToken`, else no error will be displayed in the IDE.
 
-## 15.1. Code actions plugin tutorial
+## 15.1. Language Server plugin tutorial
+
+In this section, we will create a plugin that enhances the functionality of the Language Server.
+We will start by showing the steps needed to create a plugin, followed by an example implementation that demonstrates how to provide more code actions and add custom request handlers.
 
-In this section, we will create a plugin to provide more code actions to Dafny.
-The code actions will be simple: Add a dummy comment in front of the first method name,
-if the selection is on the line of the method.
+### 15.1.1. Create plugin project
 
 Assuming the Dafny source code is installed in the folder `dafny/`
 start by creating an empty folder next to it, e.g. `PluginTutorial/`
@@ -51,22 +54,33 @@ start by creating an empty folder next to it, e.g. `PluginTutorial/`
 mkdir PluginTutorial
 cd PluginTutorial
 ```
+
 Then, create a dotnet class project
+
 ```bash
 dotnet new classlib
 ```
+
 It will create a file `Class1.cs` that you can rename
+
 ```bash
-mv Class1.cs PluginAddComment.cs
+mv Class1.cs MyPlugin.cs
 ```
+
 Open the newly created file `PluginTutorial.csproj`, and add the following after `</PropertyGroup>`:
+
 ```xml
   <ItemGroup>
     <ProjectReference Include="../dafny/source/DafnyLanguageServer/DafnyLanguageServer.csproj" />
   </ItemGroup>
 ```
+### 15.1.2. Implement plugin
+
+#### 15.1.2.1. Code actions plugin
 
-Then, open the file `PluginAddComment.cs`, remove everything, and write the imports and a namespace:
+This code action plugin will add a code action that allows you to place a dummy comment in front of the first method name, only if the selection is on the line of the method.
+
+Open the file `MyPlugin.cs`, remove everything, and write the imports and a namespace:
 
 ```csharp
 using Microsoft.Dafny;
@@ -76,18 +90,20 @@ using Microsoft.Dafny.LanguageServer.Language;
 using System.Linq;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace PluginAddComment;
+namespace MyPlugin;
 ```
 
 After that, add a `PluginConfiguration` that will expose all the quickfixers of your plugin.
 This class will be discovered and instantiated automatically by Dafny.
+
 ```csharp
 public class TestConfiguration : PluginConfiguration {
   public override DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
     return new DafnyCodeActionProvider[] { new AddCommentDafnyCodeActionProvider() };
   }
 }
 ```
+
 Note that you could also override the methods `GetRewriters()` and `GetCompilers()` for other purposes, but this is out of scope for this tutorial.
 
 Then, we need to create the quickFixer `AddCommentDafnyCodeActionProvider` itself:
@@ -102,6 +118,7 @@ public class AddCommentDafnyCodeActionProvider : DafnyCodeActionProvider {
 
 For now, this quick fixer returns nothing. `input` is the program state, and `selection` is where the caret is.
 We replace the return statement with a conditional that tests whether the selection is on the first line:
+
 ```csharp
     var firstTokenRange = input.Program?.GetFirstTopLevelToken()?.GetLspRange();
     if(firstTokenRange != null && firstTokenRange.Start.Line == selection.Start.Line) {
@@ -118,6 +135,7 @@ A `DafnyCodeActionEdit` has a `Range` to remove and some `string` to insert inst
 of the same `DafnyCodeAction` are applied at the same time if selected.
 
 To create a `DafnyCodeAction`, we can either use the easy-to-use `InstantDafnyCodeAction`, which accepts a title and an array of edits:
+
 ```csharp
   return new DafnyCodeAction[] {
     new InstantDafnyCodeAction("Insert comment", new DafnyCodeActionEdit[] {
@@ -127,6 +145,7 @@ To create a `DafnyCodeAction`, we can either use the easy-to-use `InstantDafnyCo
 ```
 
 or we can implement our custom inherited class of `DafnyCodeAction`:
+
 ```csharp
 public class CustomDafnyCodeAction: DafnyCodeAction {
   public Range whereToInsert;
@@ -141,14 +160,72 @@ public class CustomDafnyCodeAction: DafnyCodeAction {
   }
 }
 ```
+
 In that case, we could return:
+
 ```csharp
   return new DafnyCodeAction[] {
     new CustomDafnyCodeAction(firstTokenRange)
   };
 ```
 
+#### 15.1.2.2. Request handler plugin
+
+This request handler plugin enhances the Language Server to support a request with a `TextDocumentIdentifier` as parameter, which will return a `bool` value denoting whether the provided `DocumentUri` has any `LoopStmt`'s in it.
+
+Open the file `MyPlugin.cs`, remove everything, and write the imports and a namespace:
+
+```csharp
+using OmniSharp.Extensions.JsonRpc;
+using OmniSharp.Extensions.LanguageServer.Server;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Microsoft.Dafny.LanguageServer.Plugins;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using MediatR;
+using Microsoft.Dafny;
+
+namespace MyPlugin;
+```
+
+After that, add a `PluginConfiguration` that will add all the request handlers of your plugin.
+This class will be discovered and instantiated automatically by Dafny.
+
+```csharp
+public class TestConfiguration : PluginConfiguration {
+  public override LanguageServerOptions WithPluginHandlers(LanguageServerOptions options) {
+    return options.WithHandler<DummyHandler>();
+  }
+}
+```
+
+Then, we need to create the request handler `DummyHandler` itself:
+
+```csharp
+[Parallel]
+[Method("dafny/request/dummy", Direction.ClientToServer)]
+public record DummyParams : TextDocumentIdentifier, IRequest<bool>;
+
+public class DummyHandler : IJsonRpcRequestHandler<DummyParams, bool> {
+  private readonly IProjectDatabase projects;
+  public DummyHandler(IProjectDatabase projects) {
+    this.projects = projects;
+  }
+  public async Task<bool> Handle(DummyParams request, CancellationToken cancellationToken) {
+    var state = await projects.GetParsedDocumentNormalizeUri(request);
+    if (state == null) {
+      return false;
+    }
+    return state.Program.Descendants().OfType<LoopStmt>().Any();
+  }
+}
+```
+
+For more advanced example implementations of request handlers, look at `dafny/Source/DafnyLanguageServer/Handlers/*`.
+
+### 15.1.3. Building plugin
+
 That's it! Now, build your library while inside your folder:
+
 ```bash
 > dotnet build
 ```

docs/dev/news/5161.feat

@@ -0,0 +1 @@
+Allow for plugins to add custom request handlers to the language server.