From c1fe17c1cc8ea33b13f790e5191d5053a4580433 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 25 Oct 2024 12:17:40 +0200 Subject: [PATCH] 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 b0deb2ba22..4f38a9ac8f 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 72b040ad22..055760d76c 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) {