Fix LSP bug that returned a invalid range for documentSymbol

Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs

@@ -12,6 +12,31 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
   public class DocumentSymbolTest : ClientBasedLanguageServerTest {
 
+    [Fact]
+    public async Task BadReturnSyntax() {
+      var source = @"method FindZero(a: array<int>) returns (index)  // note lack of type annotation";
+      var documentItem = CreateAndOpenTestDocument(source);
+      var symbols = (await RequestDocumentSymbol(documentItem)).ToList();
+      CheckValidSymbols(symbols);
+    }
+
+    private void CheckValidSymbols(IEnumerable<DocumentSymbol> symbols) {
+      foreach (var symbol in symbols) {
+        CheckValidRange(symbol.SelectionRange);
+        CheckValidRange(symbol.Range);
+        CheckValidSymbols(symbol.Children);
+      }
+    }
+
+    private void CheckValidRange(Range range) {
+      ValidPosition(range.Start);
+      ValidPosition(range.End);
+    }
+
+    private void ValidPosition(Position position) {
+      Assert.True(position.Line >= 0 && position.Character >= 0);
+    }
+
     [Fact]
     public async Task ExportImport() {
       var source = @"

Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs

@@ -10,6 +10,7 @@
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Language;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
 namespace Microsoft.Dafny.LanguageServer.Handlers {
   /// <summary>
@@ -60,6 +61,9 @@ private IEnumerable<DocumentSymbol> FromSymbol(ISymbol symbol) {
       }
 
       var range = symbol.ToLspRange();
+      if (!IsValidRange(range)) {
+        return [];
+      }
       return new DocumentSymbol[] {
         new() {
           Children = children,
@@ -71,5 +75,13 @@ private IEnumerable<DocumentSymbol> FromSymbol(ISymbol symbol) {
         }
       };
     }
+
+    private bool IsValidRange(Range range) {
+      return IsValidPosition(range.Start) && IsValidPosition(range.End);
+    }
+
+    private bool IsValidPosition(Position position) {
+      return position.Line >= 0 && position.Character >= 0;
+    }
   }
 }

docs/dev/news/6299.fix

@@ -0,0 +1 @@
+Fix LSP bug that cause IDE exceptions during invalid parse states