Documentation on Dafny Plugin creation is not up to date (first example triggers C# compilation errors)

[ricostynha1]

What change in documentation do you suggest?

Summary

When running the current plugin creation example from the Dafny documentation:
🔗 https://dafny.org/dafny/DafnyRef/DafnyRef#sec-plugins

Specifically, the example in Section 15.1.2.1 – Code actions plugin, the provided code no longer builds successfully on the latest Dafny version.

---

Steps to Reproduce

1. Use the example code as provided at the end of section 15.1.2.1:

using Microsoft.Dafny;
using Microsoft.Dafny.LanguageServer.Plugins;
using Microsoft.Boogie;
using Microsoft.Dafny.LanguageServer.Language;
using System.Linq;
using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;

namespace MyPlugin;

public class TestConfiguration : PluginConfiguration {
  public override DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
    return new DafnyCodeActionProvider[] { new AddCommentDafnyCodeActionProvider() };
  }
}

public class AddCommentDafnyCodeActionProvider : DafnyCodeActionProvider {
  public override IEnumerable<DafnyCodeAction> GetDafnyCodeActions(IDafnyCodeActionInput input, Range selection) {
    var firstTokenRange = input.Program?.GetFirstTopLevelToken()?.GetLspRange();
    if (firstTokenRange != null && firstTokenRange.Start.Line == selection.Start.Line) {
      return new DafnyCodeAction[] {
        new InstantDafnyCodeAction("Insert comment", new DafnyCodeActionEdit[] {
          new DafnyCodeActionEdit(firstTokenRange.GetStartRange(), "/*First comment*/")
        })
      };
    } else {
      return new DafnyCodeAction[] { };
    }
  }
}

2. Build using:

   ./dafny/Binaries/Dafny --version

   Output:

   4.11.1+80a1382d7719860ec39c41c9f2fdd089657152ea
   

   and

   dotnet --version

   Output:

   8.0.117
   

3. The following compilation error occurs:

   cs(18,41): error CS1061: 'Node' does not contain a definition for 'GetFirstTopLevelToken'
   and no accessible extension method 'GetFirstTopLevelToken' accepting a first argument of
   type 'Node' could be found (are you missing a using directive or an assembly reference?)
   

---

Analysis

It seems that the API has changed in recent Dafny versions — the method GetFirstTopLevelToken() is no longer available on Node.
As a result, the documentation example no longer compiles.

---

Suggested Fix

I was able to produce a working equivalent version using StartToken instead:

using Microsoft.Dafny;
using Microsoft.Dafny.LanguageServer.Plugins;
using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;

namespace PluginAddComment;

public class TestConfiguration : PluginConfiguration {
  public override DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
    return new DafnyCodeActionProvider[] { new AddCommentDafnyCodeActionProvider() };
  }
}

public class AddCommentDafnyCodeActionProvider : DafnyCodeActionProvider {
  public override IEnumerable<DafnyCodeAction> GetDafnyCodeActions(IDafnyCodeActionInput input, Range selection) {
    var firstToken = input.Program?.StartToken;

    if (firstToken != null && firstToken.line == selection.Start.Line) {
      var start = new DafnyPosition(firstToken.line, firstToken.col);
      var dafnyRange = new DafnyRange(start, start);

      return new DafnyCodeAction[] {
        new InstantDafnyCodeAction("Insert comment", new DafnyCodeActionEdit[] {
          new DafnyCodeActionEdit(dafnyRange, "/*First comment*/")
        })
      };
    } else {
      return new DafnyCodeAction[] { };
    }
  }
}

---

Expected Outcome

• The official Dafny plugin documentation example should build successfully with the latest Dafny version (≥ 4.11).
• Updating the example to use StartToken (or the current API equivalent) would make the documentation consistent and more user-friendly for first-time plugin developers as the example would run.