fix: Document outline for functions and methods without body (#1536)

This PR resolves an issue where the document outline won't be rendered within VSCode if there are methods or functions without a body (i.e., only the signature).

The root cause is that VSCode does not render any document outline if there are symbols with invalid locations (e.g., a negative line number). The range of a declaration is computed using tok and BodyEndTok. However, BodyEndTok is set to Token.NoToken if there is no body, leading to a range ending at line -1.

Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs

@@ -138,5 +138,29 @@ method CallIt() returns () {
  Assert.AreEqual(SymbolKind.Variable, localVariableSymbol.Kind);
  Assert.AreEqual(0, localVariableSymbol.Children.Count());
  }
+
+ [TestMethod]
+ public async Task CanResolveSymbolsForMethodsWithoutBody() {
+ var source = "method DoIt()";
+ var documentItem = CreateTestDocument(source);
+ await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+ var methodSymbol = (await RequestDocumentSymbol(documentItem).AsTask()).Single().DocumentSymbol;
+ Assert.AreEqual("DoIt", methodSymbol.Name);
+ Assert.AreEqual(new Range((0, 7), (0, 11)), methodSymbol.Range);
+ Assert.AreEqual(SymbolKind.Method, methodSymbol.Kind);
+ }
+
+ [TestMethod]
+ public async Task CanResolveSymbolsForFunctionWithoutBody() {
+ var source = "function ConstOne(): int";
+ var documentItem = CreateTestDocument(source);
+ await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+
+ var methodSymbol = (await RequestDocumentSymbol(documentItem).AsTask()).Single().DocumentSymbol;
+ Assert.AreEqual("ConstOne", methodSymbol.Name);
+ Assert.AreEqual(new Range((0, 9), (0, 17)), methodSymbol.Range);
+ Assert.AreEqual(SymbolKind.Function, methodSymbol.Kind);
+ }
  }
 }

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

@@ -1,5 +1,6 @@
 using IntervalTree;
 using MediatR;
+using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Util;
 using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -77,7 +78,7 @@ public DesignatorVisitor(
  this.cancellationToken = cancellationToken;
  }
 
- public override void VisitUnknown(object node, Boogie.IToken token) {
+ public override void VisitUnknown(object node, IToken token) {
  logger.LogDebug("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})",
  node.GetType(), token.GetDocumentFileName(), token.line, token.col);
  }
@@ -283,9 +284,8 @@ public Unit Visit(FieldSymbol fieldSymbol) {
  fieldSymbol,
  fieldSymbol.Declaration.tok,
  fieldSymbol.Declaration.tok.GetLspRange(),
+ // BodyEndToken always returns Token.NoToken
  fieldSymbol.Declaration.tok.GetLspRange()
- // TODO BodyEndToken returns a token with location (0, 0)
- //new Range(fieldSymbol.Declaration.tok.GetLspPosition(), fieldSymbol.Declaration.BodyEndTok.GetLspPosition())
  );
  VisitChildren(fieldSymbol);
  return Unit.Value;
@@ -297,7 +297,7 @@ public Unit Visit(FunctionSymbol functionSymbol) {
  functionSymbol,
  functionSymbol.Declaration.tok,
  functionSymbol.Declaration.tok.GetLspRange(),
- new Range(functionSymbol.Declaration.tok.GetLspPosition(), functionSymbol.Declaration.BodyEndTok.GetLspPosition())
+ GetDeclarationRange(functionSymbol.Declaration)
  );
  VisitChildren(functionSymbol);
  return Unit.Value;
@@ -309,12 +309,18 @@ public Unit Visit(MethodSymbol methodSymbol) {
  methodSymbol,
  methodSymbol.Declaration.tok,
  methodSymbol.Declaration.tok.GetLspRange(),
- new Range(methodSymbol.Declaration.tok.GetLspPosition(), methodSymbol.Declaration.BodyEndTok.GetLspPosition())
+ GetDeclarationRange(methodSymbol.Declaration)
  );
  VisitChildren(methodSymbol);
  return Unit.Value;
  }
 
+ private static Range GetDeclarationRange(Declaration declaration) {
+ return declaration.BodyEndTok == Token.NoToken
+ ? declaration.tok.GetLspRange()
+ : new Range(declaration.tok.GetLspPosition(), declaration.BodyEndTok.GetLspPosition());
+ }
+
  public Unit Visit(VariableSymbol variableSymbol) {
  cancellationToken.ThrowIfCancellationRequested();
  RegisterLocation(
@@ -345,7 +351,7 @@ private void VisitChildren(ISymbol symbol) {
  }
  }
 
- private void RegisterLocation(ISymbol symbol, Boogie.IToken token, Range name, Range declaration) {
+ private void RegisterLocation(ISymbol symbol, IToken token, Range name, Range declaration) {
  if (token.filename != null) {
  // The filename is null if we have a default or System based symbol. This is also reflected by the ranges being usually -1.
  Locations.Add(symbol, new SymbolLocation(token.GetDocumentUri(), name, declaration));