Fixed the CI tests

Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs

@@ -0,0 +1,67 @@
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using OmniSharp.Extensions.LanguageServer.Protocol.Document;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using System.Collections.Generic;
+using System.Linq;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+using Xunit.Abstractions;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Completion {
+  public class AtCompletionTest : ClientBasedLanguageServerTest {
+
+    private async Task<List<CompletionItem>> RequestCompletionAsync(TextDocumentItem documentItem, Position position) {
+      var completionList = await client.RequestCompletion(
+        new CompletionParams {
+          TextDocument = documentItem.Uri,
+          Position = position
+        },
+        CancellationToken
+      ).AsTask();
+      return completionList.OrderBy(completion => completion.Label).ToList();
+    }
+
+    [Fact]
+    public async Task CompleteNoAtAttributeDuringAtCall() {
+      var source = @"
+method Foo() { label start: previous@(x); }".TrimStart();
+      var documentItem = CreateAndOpenTestDocument(source, "CompleteAtCall.dfy");
+
+      var completionList = await RequestCompletionAsync(documentItem, (0, 37));
+      Assert.Empty(completionList);
+    }
+
+    private static void AssertEqualToAllCompletions(List<CompletionItem> completionList) {
+      Assert.Equal(Attributes.BuiltinAtAttributes.Count, completionList.Count);
+      for (var i = 0; i < completionList.Count; i++) {
+        Assert.Equal(Attributes.BuiltinAtAttributes[0].Name, completionList[0].Label);
+        Assert.Equal(CompletionItemKind.Constructor, completionList[1].Kind);
+      }
+    }
+
+    [Fact]
+    public async Task CompleteAtAttributeBeforeMethod() {
+      var source = @"
+/* Does what is expected */ @ method Foo() { }".TrimStart();
+      var documentItem = CreateTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var completionList = await RequestCompletionAsync(documentItem, (0, 29));
+      AssertEqualToAllCompletions(completionList);
+    }
+
+    [Fact]
+    public async Task CompleteAtAttributeBeforeMethodAfterNewline() {
+      var source = @"
+/* Does what is expected */".TrimStart() + "\n" +
+"@ method Foo() { }".TrimStart();
+      var documentItem = CreateTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var completionList = await RequestCompletionAsync(documentItem, (1, 1));
+      AssertEqualToAllCompletions(completionList);
+    }
+
+    public AtCompletionTest(ITestOutputHelper output) : base(output) {
+    }
+  }
+}

Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs

@@ -93,29 +93,41 @@ public CompletionList Process() {
         return new CompletionList();
       }
 
-      private static string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) {
+      private string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) {
         // To track the last two characters
         char? prevChar = null;
         char? currentChar = null;
+        var targetLineIndex = position.Line;
+        var targetColumnIndex = position.Column - 1;
 
         // Read line by line
-        for (int lineNum = 0; lineNum <= position.Line; lineNum++) {
-          string? line = fileContent.ReadLine();
+        for (var lineNum = 0; lineNum <= targetLineIndex; lineNum++) {
+          var line = fileContent.ReadLine();
           if (line == null) {
-            throw new InvalidOperationException("Reached end of file before finding the specified line.");
+            logger.LogWarning("Reached end of file before finding the specified line.");
+            return "";
           }
 
           // If we are on the line of the specified position, handle the partial line case
-          if (lineNum == position.Line) {
-            int columnIndex = position.Column - 1; // Convert 1-based to 0-based index
+          if (lineNum == targetLineIndex) {
+            int columnIndex = targetColumnIndex; // Convert 1-based to 0-based index
             for (int i = 0; i <= columnIndex; i++) {
               prevChar = currentChar;
-              currentChar = line[i];
+              if (line.Length <= i) { // In some tests (e.g. SlowlyTypeFile) the position is given only as a character index
+                targetLineIndex += 1;
+                targetColumnIndex -= line.Length + 1; // 1 for the newline. It does not need to be OS-specific, since it's just for a coverage test
+              } else {
+                currentChar = line[i];
+              }
+            }
+
+            if (lineNum < targetLineIndex) {
+              continue;
             }
             break;
           } else {
             // Otherwise, track the last two characters of this full line (including newline)
-            foreach (char c in line + '\n')  // Include '\n' for line end tracking
+            foreach (var c in line + '\n')  // Include '\n' for line end tracking
             {
               prevChar = currentChar;
               currentChar = c;