diff --git a/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs new file mode 100644 index 00000000000..6a064e868ce --- /dev/null +++ b/Source/DafnyLanguageServer.Test/Completion/AtCompletionTest.cs @@ -0,0 +1,76 @@ +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 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, "CompleteAtBeforeMethod.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.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.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/DafnyCompletionHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs index 9bf8edc6313..5d188ea4138 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyCompletionHandler.cs @@ -12,27 +12,30 @@ 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) { return new CompletionRegistrationOptions { DocumentSelector = DocumentSelector.ForLanguage("dafny"), ResolveProvider = false, - TriggerCharacters = new Container(".") + TriggerCharacters = new Container(".", "@") }; } @@ -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).Process(); + return new CompletionProcessor(symbolGuesser, logger, document, request, cancellationToken, options, filesystem).Process(); } private class CompletionProcessor { @@ -59,15 +62,18 @@ private class CompletionProcessor { private readonly IdeState state; private readonly CompletionParams request; private readonly CancellationToken cancellationToken; + private readonly LanguageServerFilesystem filesystem; public CompletionProcessor(ISymbolGuesser symbolGuesser, ILogger logger, IdeState state, - CompletionParams request, CancellationToken cancellationToken, DafnyOptions options) { + CompletionParams request, CancellationToken cancellationToken, DafnyOptions options, + LanguageServerFilesystem filesystem) { this.symbolGuesser = symbolGuesser; this.state = state; this.request = request; this.cancellationToken = cancellationToken; this.options = options; this.logger = logger; + this.filesystem = filesystem; } public CompletionList Process() { @@ -75,6 +81,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 +96,43 @@ public CompletionList Process() { return new CompletionList(); } + private string GetLastTwoCharactersBeforePositionIncluded(TextBuffer text, DafnyPosition position) { + var index = text.ToIndex(position.GetLspPosition()); + var indexTwoCharactersBefore = Math.Max(0, index - 2); + if (index > text.Text.Length) { + return ""; + } + + return text.Text.Substring(indexTwoCharactersBefore, index - indexTwoCharactersBefore); + } + 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(); + var fileContent = filesystem.GetBuffer(request.TextDocument.Uri.ToUri()); + if (fileContent == null) { + // Impossible case because this only happens if the file is not opened. + return false; + } + 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 +164,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, + Detail = "" + }; + } + private CompletionItem CreateCompletionItem(ILegacySymbol symbol) { return new CompletionItem { Label = symbol.Name, 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 diff --git a/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs b/Source/DafnyLanguageServer/Workspace/LanguageServerFilesystem.cs index 415ba1e1109..33ebc79dffe 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 null; + } + 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 9498e3ba546..3e58f730413 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; diff --git a/Source/DafnyLanguageServer/Workspace/TextBuffer.cs b/Source/DafnyLanguageServer/Workspace/TextBuffer.cs index 72b040ad22c..642a27afa23 100644 --- a/Source/DafnyLanguageServer/Workspace/TextBuffer.cs +++ b/Source/DafnyLanguageServer/Workspace/TextBuffer.cs @@ -57,7 +57,15 @@ public Position FromIndex(int index) { } private BufferLine IndexToLine(int index) { - return indexToLineTree.Query(index).Single(); + try { + return indexToLineTree.Query(index).Single(); + } catch (InvalidOperationException) { + try {// Just in case we are on Windows and we happen to query an index between "\r" and "\n" + return indexToLineTree.Query(index - 1).Single(); + } catch (InvalidOperationException) { + throw new ArgumentException($"index {index} is outside of the text buffer"); + } + } } public int ToIndex(Position position) {