Skip to content

Commit

Permalink
Fix to SlowlyTypeFile
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Oct 25, 2024
1 parent 9c22929 commit c1fe17c
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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;
}
}
Expand Down
6 changes: 5 additions & 1 deletion Source/DafnyLanguageServer/Workspace/TextBuffer.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down

0 comments on commit c1fe17c

Please sign in to comment.