From 52e506e0e4e29d226dc490c904e65ebc03d0b46f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 17 Oct 2024 10:51:30 -0500 Subject: [PATCH 1/9] Feat: Auto-completion of @-attributes for the language server --- .../Handlers/DafnyCompletionHandler.cs | 80 ++++++++++++++++++- .../Workspace/ProjectManager.cs | 5 ++ 2 files changed, 82 insertions(+), 3 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 9bf8edc6313..89ed6dddcdd 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -32,7 +32,7 @@ protected override CompletionRegistrationOptions CreateRegistrationOptions(Compl return new CompletionRegistrationOptions { DocumentSelector = DocumentSelector.ForLanguage("dafny"), ResolveProvider = false, - TriggerCharacters = new Container(".") + TriggerCharacters = new Container(".", "@") }; } @@ -49,7 +49,7 @@ public override async Task Handle(CompletionParams request, Canc logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return new CompletionList(); } - return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options).Process(); + return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, await projects.GetProjectManager(request.TextDocument.Uri)).Process(); } private class CompletionProcessor { @@ -59,15 +59,18 @@ private class CompletionProcessor { private readonly IdeState state; private readonly CompletionParams request; private readonly CancellationToken cancellationToken; + private readonly ProjectManager? projectManager; public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger logger, IdeState state, - CompletionParams request, CancellationToken cancellationToken, DafnyOptions options) { + CompletionParams request, CancellationToken cancellationToken, DafnyOptions options, + ProjectManager? projectManager) { this.symbolGuesser = symbolGuesser; this.state = state; this.request = request; this.cancellationToken = cancellationToken; this.options = options; this.logger = logger; + this.projectManager = projectManager; } public CompletionList Process() { @@ -75,6 +78,10 @@ public CompletionList Process() { return CreateDotCompletionList(); } + if (IsAtAttribute()) { + return CreateAtAttributeCompletionList(); + } + if (logger.IsEnabled(LogLevel.Trace)) { var program = (Program)state.ResolvedProgram!; var writer = new StringWriter(); @@ -86,11 +93,69 @@ public CompletionList Process() { return new CompletionList(); } + private static string GetLastTwoCharactersBeforePositionIncluded(TextReader fileContent, DafnyPosition position) { + // To track the last two characters + char? prevChar = null; + char? currentChar = null; + + // Read line by line + for (int lineNum = 0; lineNum <= position.Line; lineNum++) { + string? line = fileContent.ReadLine(); + if (line == null) { + throw new InvalidOperationException("Reached end of file before finding the specified line."); + } + + // 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 + for (int i = 0; i <= columnIndex; i++) { + prevChar = currentChar; + currentChar = line[i]; + } + 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 + { + prevChar = currentChar; + currentChar = c; + } + } + } + + // Handle case where fewer than 2 characters are available + if (prevChar == null) { + return currentChar?.ToString() ?? ""; + } + return $"{prevChar}{currentChar}"; + } + private bool IsDotExpression() { var node = state.Program.FindNode(request.TextDocument.Uri.ToUri(), request.Position.ToDafnyPosition()); return node?.RangeToken.EndToken.val == "."; } + private bool IsAtAttribute() { + var position = request.Position.ToDafnyPosition(); + if (projectManager == null) { + return false; + } + var fileContent = projectManager.ReadFile(request.TextDocument.Uri.ToUri()); + var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position); + var isAtAttribute = + lastTwoChars == "@" || + lastTwoChars.Length >= 2 && lastTwoChars[1] == '@' && char.IsWhiteSpace(lastTwoChars[0]); + return isAtAttribute; + } + + private CompletionList CreateAtAttributeCompletionList() { + var completionItems = + Attributes.BuiltinAtAttributes.Select(b => + CreateCompletionItem(b.Name) + ).ToList(); + return new CompletionList(completionItems); + } + private CompletionList CreateDotCompletionList() { IEnumerable members; if (symbolGuesser.TryGetTypeBefore(state, @@ -122,6 +187,15 @@ private static bool IsConstructor(ILegacySymbol symbol) { return symbol is MethodSymbol method && method.Name == "_ctor"; } + private CompletionItem CreateCompletionItem(string attributeName) { + return new CompletionItem { + Label = attributeName, + Kind = CompletionItemKind.Constructor, + InsertText = attributeName, // TODO: Parentheses + Detail = "" // TODO: Details of attribute name + }; + } + private CompletionItem CreateCompletionItem(ILegacySymbol symbol) { return new CompletionItem { Label = symbol.Name, diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index 9498e3ba546..09bff0e2723 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -2,6 +2,7 @@ using System.Collections.Concurrent; using System.Collections.Generic; using System.CommandLine; +using System.IO; using System.Linq; using System.Numerics; using System.Reactive.Concurrency; @@ -126,6 +127,10 @@ public ProjectManager( private const int MaxRememberedChanges = 100; + public TextReader ReadFile(Uri fileToRead) { + return fileSystem.ReadFile(fileToRead); + } + public void UpdateDocument(DidChangeTextDocumentParams documentChange) { StartNewCompilation(documentChange.TextDocument.Uri.ToUri(), documentChange); } From 92dc32f10c1b50e282136aff9f36bffe3bbbf97b Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 21 Oct 2024 15:27:47 -0500 Subject: [PATCH 2/9] Fixed the CI tests --- .../Completion/AtCompletionTest.cs | 67 +++++++++++++++++++ .../Handlers/DafnyCompletionHandler.cs | 28 +++++--- 2 files changed, 87 insertions(+), 8 deletions(-) create mode 100644 Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs diff --git a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs new file mode 100644 index 00000000000..0c1fa5accc6 --- /dev/null +++ b/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> 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 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) { + } + } +} diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 89ed6dddcdd..6fb8a682795 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/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; From 18792b627b8d29b84f5b10e0136fc14789f75823 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Oct 2024 11:14:23 +0200 Subject: [PATCH 3/9] Use a TextBuffer instead of a FileReader --- .../Handlers/DafnyCompletionHandler.cs | 69 ++++--------------- .../Workspace/LanguageServerFilesystem.cs | 8 +++ .../Workspace/ProjectManager.cs | 4 -- 3 files changed, 21 insertions(+), 60 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 6fb8a682795..bd5bc8e543d 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -12,20 +12,23 @@ using System.Linq; using System.Threading; using System.Threading.Tasks; +using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range; namespace Microsoft.Dafny.LanguageServer.Handlers { public class DafnyCompletionHandler : CompletionHandlerBase { private readonly ILogger logger; private readonly IProjectDatabase projects; + private readonly LanguageServerFilesystem filesystem; private readonly ISymbolGuesser symbolGuesser; private DafnyOptions options; public DafnyCompletionHandler(ILogger logger, IProjectDatabase projects, - ISymbolGuesser symbolGuesser, DafnyOptions options) { + ISymbolGuesser symbolGuesser, DafnyOptions options, LanguageServerFilesystem filesystem) { this.logger = logger; this.projects = projects; this.symbolGuesser = symbolGuesser; this.options = options; + this.filesystem = filesystem; } protected override CompletionRegistrationOptions CreateRegistrationOptions(CompletionCapability capability, ClientCapabilities clientCapabilities) { @@ -49,7 +52,7 @@ public override async Task Handle(CompletionParams request, Canc logger.LogWarning("location requested for unloaded document {DocumentUri}", request.TextDocument.Uri); return new CompletionList(); } - return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, await projects.GetProjectManager(request.TextDocument.Uri)).Process(); + return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, filesystem).Process(); } private class CompletionProcessor { @@ -59,18 +62,18 @@ private class CompletionProcessor { private readonly IdeState state; private readonly CompletionParams request; private readonly CancellationToken cancellationToken; - private readonly ProjectManager? projectManager; + private readonly LanguageServerFilesystem filesystem; public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger logger, IdeState state, CompletionParams request, CancellationToken cancellationToken, DafnyOptions options, - ProjectManager? projectManager) { + LanguageServerFilesystem filesystem) { this.symbolGuesser = symbolGuesser; this.state = state; this.request = request; this.cancellationToken = cancellationToken; this.options = options; this.logger = logger; - this.projectManager = projectManager; + this.filesystem = filesystem; } public CompletionList Process() { @@ -93,53 +96,10 @@ public CompletionList Process() { return new CompletionList(); } - 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 (var lineNum = 0; lineNum <= targetLineIndex; lineNum++) { - var line = fileContent.ReadLine(); - if (line == null) { - 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 == targetLineIndex) { - int columnIndex = targetColumnIndex; // Convert 1-based to 0-based index - for (int i = 0; i <= columnIndex; i++) { - prevChar = currentChar; - 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 (var c in line + '\n') // Include '\n' for line end tracking - { - prevChar = currentChar; - currentChar = c; - } - } - } - - // Handle case where fewer than 2 characters are available - if (prevChar == null) { - return currentChar?.ToString() ?? ""; - } - return $"{prevChar}{currentChar}"; + private string GetLastTwoCharactersBeforePositionIncluded(TextBuffer text, DafnyPosition position) { + var index = text.ToIndex(position.GetLspPosition()); + var beforePosition = text.FromIndex(Math.Max(0, index - 2)); + return text.Extract(new Range(beforePosition, position.GetLspPosition())); } private bool IsDotExpression() { @@ -149,10 +109,7 @@ private bool IsDotExpression() { private bool IsAtAttribute() { var position = request.Position.ToDafnyPosition(); - if (projectManager == null) { - return false; - } - var fileContent = projectManager.ReadFile(request.TextDocument.Uri.ToUri()); + var fileContent = filesystem.GetBuffer(request.TextDocument.Uri.ToUri()); var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position); var isAtAttribute = lastTwoChars == "@" || diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs index 415ba1e1109..d8bc48e3f3f 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs @@ -89,6 +89,14 @@ public void CloseDocument(TextDocumentIdentifier document) { } } + public TextBuffer GetBuffer(Uri uri) { + if (openFiles.TryGetValue(uri, out var entry)) { + return entry.Buffer; + } + + return new TextBuffer(OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd()); + } + public TextReader ReadFile(Uri uri) { if (openFiles.TryGetValue(uri, out var entry)) { return new StringReader(entry.Buffer.Text); diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index 09bff0e2723..3e58f730413 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -127,10 +127,6 @@ public ProjectManager( private const int MaxRememberedChanges = 100; - public TextReader ReadFile(Uri fileToRead) { - return fileSystem.ReadFile(fileToRead); - } - public void UpdateDocument(DidChangeTextDocumentParams documentChange) { StartNewCompilation(documentChange.TextDocument.Uri.ToUri(), documentChange); } From 56fd9795a47cbac5afaa4a32ad9938c0fb2921aa Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Oct 2024 11:15:00 +0200 Subject: [PATCH 4/9] Clean up some garbage code --- .../Unit/TextDocumentLoaderTest.cs | 9 ---- .../Handlers/DafnyTextDocumentHandler.cs | 2 +- .../Workspace/DocumentTextBuffer.cs | 42 ------------------- 3 files changed, 1 insertion(+), 52 deletions(-) delete mode 100644 Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs index 9a5a4b78416..5ec823455e8 100644 --- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs +++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs @@ -44,15 +44,6 @@ private static VersionedTextDocumentIdentifier CreateTestDocumentId() { }; } - private static DocumentTextBuffer CreateTestDocument() { - return new DocumentTextBuffer(new TextDocumentItem() { - Uri = DocumentUri.Parse("untitled:untitled1"), - LanguageId = "dafny", - Version = 1, - Text = "" - }); - } - [Fact] public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() { var source = new CancellationTokenSource(); diff --git a/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs index 7bfb738d174..c13b9e91a20 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs @@ -62,7 +62,7 @@ public override TextDocumentAttributes GetTextDocumentAttributes(DocumentUri uri public override async Task Handle(DidOpenTextDocumentParams notification, CancellationToken cancellationToken) { logger.LogDebug("received open notification {DocumentUri}", notification.TextDocument.Uri); try { - await projects.OpenDocument(new DocumentTextBuffer(notification.TextDocument)); + await projects.OpenDocument(notification.TextDocument); } catch (InvalidOperationException e) { if (!e.Message.Contains("because it is already open")) { telemetryPublisher.PublishUnhandledException(e); diff --git a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs b/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs deleted file mode 100644 index c28f12da43b..00000000000 --- a/Source/DafnyLanguageServer/Workspace/DocumentTextBuffer.cs +++ /dev/null @@ -1,42 +0,0 @@ -using System.IO; -using System.Net.Mime; -using OmniSharp.Extensions.LanguageServer.Protocol; -using OmniSharp.Extensions.LanguageServer.Protocol.Models; - -namespace Microsoft.Dafny.LanguageServer.Workspace; - -public class DocumentTextBuffer { - public TextDocumentItem TextDocumentItem { get; } - public TextBuffer Buffer { get; } - public DocumentTextBuffer(TextDocumentItem documentItem) { - TextDocumentItem = documentItem; - Buffer = new TextBuffer(documentItem.Text); - } - - public DocumentTextBuffer(TextDocumentItem documentItem, TextBuffer buffer) { - TextDocumentItem = documentItem; - Buffer = buffer; - } - - public Range Range => new Range(0, 0, NumberOfLines, 0); - - public Position FromIndex(int index) { - return Buffer.FromIndex(index); - } - - public int ToIndex(Position position) { - return Buffer.ToIndex(position); - } - - public string Extract(Range range) { - return Buffer.Extract(range); - } - - public static implicit operator TextDocumentItem(DocumentTextBuffer buffer) => buffer.TextDocumentItem; - public string Text => TextDocumentItem.Text; - public DocumentUri Uri => TextDocumentItem.Uri; - public int? Version => TextDocumentItem.Version; - - public int NumberOfLines => Buffer.Lines.Count; - public TextReader Content => new StringReader(Text); -} \ No newline at end of file From 3f24148ee45a3f858f5d9b2ce999be683c76ba5b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Oct 2024 11:16:24 +0200 Subject: [PATCH 5/9] Little bit of cleanup --- Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs | 4 ++++ .../DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index bd5bc8e543d..08ae35da16e 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -110,6 +110,10 @@ private bool IsDotExpression() { private bool IsAtAttribute() { var position = request.Position.ToDafnyPosition(); var fileContent = filesystem.GetBuffer(request.TextDocument.Uri.ToUri()); + if (fileContent == null) { + // Impossible case because this only happens if the is not opened. + return false; + } var lastTwoChars = GetLastTwoCharactersBeforePositionIncluded(fileContent, position); var isAtAttribute = lastTwoChars == "@" || diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs index d8bc48e3f3f..33ebc79dffe 100644 --- a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs +++ b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs @@ -89,12 +89,12 @@ public void CloseDocument(TextDocumentIdentifier document) { } } - public TextBuffer GetBuffer(Uri uri) { + public TextBuffer? GetBuffer(Uri uri) { if (openFiles.TryGetValue(uri, out var entry)) { return entry.Buffer; } - return new TextBuffer(OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd()); + return null; } public TextReader ReadFile(Uri uri) { From 357b0aceb4d4b14fc34ed8f2ec8a5c582b0129d5 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 24 Oct 2024 15:24:14 -0500 Subject: [PATCH 6/9] Added test for a @ character at the beginning of the file --- .../Completion/AtCompletionTest.cs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs index 0c1fa5accc6..dbf47f59543 100644 --- a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs +++ b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs @@ -39,12 +39,21 @@ private static void AssertEqualToAllCompletions(List completionL Assert.Equal(CompletionItemKind.Constructor, completionList[1].Kind); } } + + [Fact] + public async Task CompleteAtAttributeAtBeginningOfFile() { + var source = @"@"; + var documentItem = CreateTestDocument(source, "CompleteAt.dfy"); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + var completionList = await RequestCompletionAsync(documentItem, (0, 1)); + AssertEqualToAllCompletions(completionList); + } [Fact] public async Task CompleteAtAttributeBeforeMethod() { var source = @" /* Does what is expected */ @ method Foo() { }".TrimStart(); - var documentItem = CreateTestDocument(source, "CompleteOnThisReturnsClassMembers.dfy"); + var documentItem = CreateTestDocument(source, "CompleteAtBeforeMethod.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var completionList = await RequestCompletionAsync(documentItem, (0, 29)); AssertEqualToAllCompletions(completionList); From 9c22929a7660b58037494ce62e72355c1cdb007d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 24 Oct 2024 15:26:40 -0500 Subject: [PATCH 7/9] Formatting --- .../DafnyLanguageServer.Test/Completion/AtCompletionTest.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs index dbf47f59543..6a064e868ce 100644 --- a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs +++ b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs @@ -39,10 +39,10 @@ private static void AssertEqualToAllCompletions(List completionL Assert.Equal(CompletionItemKind.Constructor, completionList[1].Kind); } } - + [Fact] public async Task CompleteAtAttributeAtBeginningOfFile() { - var source = @"@"; + var source = "@"; var documentItem = CreateTestDocument(source, "CompleteAt.dfy"); await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); var completionList = await RequestCompletionAsync(documentItem, (0, 1)); From c1fe17c1cc8ea33b13f790e5191d5053a4580433 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 25 Oct 2024 12:17:40 +0200 Subject: [PATCH 8/9] Fix to SlowlyTypeFile --- .../Synchronization/EditDocumentTest.cs | 8 +++++--- Source/DafnyLanguageServer/Workspace/TextBuffer.cs | 6 +++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs index b0deb2ba224..4f38a9ac8fb 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/EditDocumentTest.cs @@ -223,7 +223,8 @@ await SetUp(dafnyOptions => { var buffer = new TextBuffer(""); foreach (var midPart in sourceParts) { for (var midIndex = 0; midIndex < midPart.Length; midIndex += stepSize) { - var part = midPart.Substring(midIndex, Math.Min(midPart.Length, midIndex + stepSize) - midIndex); + var length = Math.Min(midPart.Length, midIndex + stepSize) - midIndex; + var part = midPart.Substring(midIndex, length); var cursorIndex = index + part.Length; var position = buffer.FromIndex(index); @@ -234,8 +235,9 @@ await SetUp(dafnyOptions => { ApplyChange(ref document, new Range(position, position), part); await WaitUntilResolutionFinished(document); - var completionItems = await RequestCompletionAsync(document, new Position(0, midIndex + stepSize)); - var hover = await RequestHover(document, new Position(0, midIndex + stepSize)); + var position2 = buffer.FromIndex(midIndex + length); + var completionItems = await RequestCompletionAsync(document, position2); + var hover = await RequestHover(document, position2); index = cursorIndex; } } diff --git a/Source/DafnyLanguageServer/Workspace/TextBuffer.cs b/Source/DafnyLanguageServer/Workspace/TextBuffer.cs index 72b040ad22c..055760d76cc 100644 --- a/Source/DafnyLanguageServer/Workspace/TextBuffer.cs +++ b/Source/DafnyLanguageServer/Workspace/TextBuffer.cs @@ -57,7 +57,11 @@ public Position FromIndex(int index) { } private BufferLine IndexToLine(int index) { - return indexToLineTree.Query(index).Single(); + try { + return indexToLineTree.Query(index).Single(); + } catch (InvalidOperationException) { + throw new ArgumentException($"index {index} is outside of the text buffer"); + } } public int ToIndex(Position position) { From ccb30b2a138e6304116a1237a16b1ca96c317a04 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 28 Oct 2024 06:21:59 -0500 Subject: [PATCH 9/9] Removed the TODOs, will be done later --- Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 08ae35da16e..e55ba172eed 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -164,8 +164,8 @@ private CompletionItem CreateCompletionItem(string attributeName) { return new CompletionItem { Label = attributeName, Kind = CompletionItemKind.Constructor, - InsertText = attributeName, // TODO: Parentheses - Detail = "" // TODO: Details of attribute name + InsertText = attributeName, + Detail = "" }; }