feat: Add customized folding ranges to the dafny document

Source/DafnyLanguageServer/Handlers/DafnyFoldingRangeHandler.cs

@@ -0,0 +1,43 @@
+using Microsoft.Dafny.LanguageServer.Language.Symbols;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol.Client.Capabilities;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using System;
+using System.Linq;
+using System.Threading;
+using System.Threading.Tasks;
+
+namespace Microsoft.Dafny.LanguageServer.Handlers {
+ /// <summary>
+ /// LSP Synchronization handler for symbol based events, i.e. the client requests the symbols of the specified document.
+ /// </summary>
+ public class DafnyFoldingRangeHandler : FoldingRangeHandlerBase {
+ private static readonly SymbolInformationOrDocumentSymbol[] EmptySymbols = Array.Empty<SymbolInformationOrDocumentSymbol>();
+
+ private readonly ILogger logger;
+ private readonly IDocumentDatabase documents;
+
+ public DafnyFoldingRangeHandler(ILogger<DafnyDocumentSymbolHandler> logger, IDocumentDatabase documents) {
+ this.logger = logger;
+ this.documents = documents;
+ }
+
+ protected override FoldingRangeRegistrationOptions CreateRegistrationOptions(FoldingRangeCapability capability, ClientCapabilities clientCapabilities) {
+ return new FoldingRangeRegistrationOptions {
+ DocumentSelector = DocumentSelector.ForLanguage("dafny")
+ };
+ }
+
+ public async override Task<Container<FoldingRange>?> Handle(FoldingRangeRequestParam request, CancellationToken cancellationToken) {
+ var document = await documents.GetResolvedDocumentAsync(request.TextDocument);
+ if (document == null) {
+ logger.LogWarning("symbols requested for unloaded document {DocumentUri}", request.TextDocument.Uri);
+ return null;
+ }
+ var visitor = new LspFoldingRangeGeneratingVisitor(document.SymbolTable, cancellationToken);
+ return visitor.Visit(document.SymbolTable.CompilationUnit).ToArray();
+ }
+ }
+}

Source/DafnyLanguageServer/Handlers/LanguageServerExtensions.cs

@@ -21,7 +21,8 @@ public static class LanguageServerExtensions {
  .WithHandler<DafnyCompletionHandler>()
  .WithHandler<DafnySignatureHelpHandler>()
  .WithHandler<DafnyCounterExampleHandler>()
- .WithHandler<VerificationHandler>();
+ .WithHandler<VerificationHandler>()
+ .WithHandler<DafnyFoldingRangeHandler>();
  }
  }
 }

Source/DafnyLanguageServer/Language/Symbols/LspFoldingRangeGeneratingVisitor.cs

@@ -0,0 +1,105 @@
+using Microsoft.Dafny.LanguageServer.Util;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using System.Collections.Generic;
+using System.Linq;
+using System.Threading;
+
+namespace Microsoft.Dafny.LanguageServer.Language.Symbols {
+ /// <summary>
+ /// Visitor responsible to generate the LSP foldable ranges.
+ /// </summary>
+ public class LspFoldingRangeGeneratingVisitor : ISymbolVisitor<IEnumerable<FoldingRange>> {
+ private readonly SymbolTable symbolTable;
+ private readonly CancellationToken cancellationToken;
+
+ public LspFoldingRangeGeneratingVisitor(SymbolTable symbolTable, CancellationToken cancellationToken) {
+ this.symbolTable = symbolTable;
+ this.cancellationToken = cancellationToken;
+ }
+
+ private bool IsPartOfEntryDocument(Boogie.IToken token) {
+ // Tokens with line=0 usually represent a default/implicit class/module/etc. We do not want
+ // to show these in the symbol listing.
+ return token.line != 0 && symbolTable.CompilationUnit.Program.IsPartOfEntryDocument(token);
+ }
+
+ public IEnumerable<FoldingRange> Visit(ISymbol symbol) {
+ cancellationToken.ThrowIfCancellationRequested();
+ return symbol.Accept(this);
+ }
+
+ public IEnumerable<FoldingRange> Visit(CompilationUnit compilationUnit) {
+ return compilationUnit.Children.SelectMany(Visit).ToArray();
+ }
+
+ public IEnumerable<FoldingRange> Visit(ModuleSymbol moduleSymbol) {
+ return CreateFoldingRangesOfEntryDocument(moduleSymbol, moduleSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(ClassSymbol classSymbol) {
+ return CreateFoldingRangesOfEntryDocument(classSymbol, classSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(DataTypeSymbol dataTypeSymbol) {
+ return CreateFoldingRangesOfEntryDocument(dataTypeSymbol, dataTypeSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(ValueTypeSymbol valueTypeSymbol) {
+ return CreateFoldingRangesOfEntryDocument(valueTypeSymbol, valueTypeSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(FieldSymbol fieldSymbol) {
+ return CreateFoldingRangesOfEntryDocument(fieldSymbol, fieldSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(FunctionSymbol functionSymbol) {
+ return CreateFoldingRangesOfEntryDocument(functionSymbol, functionSymbol.Declaration.tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(MethodSymbol methodSymbol) {
+ if (methodSymbol.Declaration.Body == null || !symbolTable.TryGetLocationOf(methodSymbol, out var location)) {
+ return VisitChildren(methodSymbol);
+ }
+ if (methodSymbol.Returns.Count == 0 || !symbolTable.TryGetLocationOf(methodSymbol.Returns[^1], out var lastReturnLocation)) {
+ return CreateFoldingRangesOfEntryDocument(methodSymbol, methodSymbol.Declaration.tok, location.Declaration);
+ }
+ var range = new Range(
+ lastReturnLocation.Declaration.End,
+ location.Declaration.End
+ );
+ return CreateFoldingRangesOfEntryDocument(methodSymbol, methodSymbol.Declaration.tok, range);
+ }
+
+ public IEnumerable<FoldingRange> Visit(VariableSymbol variableSymbol) {
+ return CreateFoldingRangesOfEntryDocument(variableSymbol, variableSymbol.Declaration.Tok);
+ }
+
+ public IEnumerable<FoldingRange> Visit(ScopeSymbol scopeSymbol) {
+ return CreateFoldingRangesOfEntryDocument(scopeSymbol, scopeSymbol.BodyStartToken);
+ }
+
+ private IEnumerable<FoldingRange> CreateFoldingRangesOfEntryDocument(ILocalizableSymbol symbol, Boogie.IToken token) {
+ if (!symbolTable.TryGetLocationOf(symbol, out var location)) {
+ return VisitChildren(symbol);
+ }
+ return CreateFoldingRangesOfEntryDocument(symbol, token, location.Declaration);
+ }
+
+ private IEnumerable<FoldingRange> CreateFoldingRangesOfEntryDocument(ILocalizableSymbol symbol, Boogie.IToken token, Range range) {
+ var children = VisitChildren(symbol);
+ if (!IsPartOfEntryDocument(token)) {
+ return children;
+ }
+ return children.Append(new FoldingRange {
+ StartLine = range.Start.Line,
+ StartCharacter = range.Start.Character,
+ EndLine = range.End.Line,
+ EndCharacter = range.End.Character
+ });
+ }
+
+ private IEnumerable<FoldingRange> VisitChildren(ISymbol symbol) {
+ return symbol.Children.SelectMany(Visit);
+ }
+ }
+}