Skip to content

Commit

Permalink
Prevent the IDE from locking up when certain parse error occur (#4495)
Browse files Browse the repository at this point in the history
### Changes

Previously the IDE server would become completely unresponsive when a
repeated comma occurred in a parameter, now it does not.

### Testing

Added test to ensure the behavior does not occur

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer committed Sep 19, 2023
1 parent 532fb7f commit 7d93b88
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 1 deletion.
6 changes: 5 additions & 1 deletion Source/DafnyCore/Generic/Node.cs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,11 @@ public IEnumerable<IToken> OwnedTokens {
var childrenFiltered = GetConcreteChildren(this).ToList();

// If we parse a resolved document, some children sometimes have the same token because they are auto-generated
var startToEndTokenNotOwned = childrenFiltered.GroupBy(child => child.StartToken.pos).
var startToEndTokenNotOwned = childrenFiltered.
// Because RangeToken.EndToken is inclusive, a token with an empty range has an EndToken that occurs before the StartToken
// We need to filter these out to prevent an infinite loop
Where(c => c.StartToken.pos <= c.EndToken.pos).
GroupBy(child => child.StartToken.pos).
ToDictionary(g => g.Key, g => g.MaxBy(child => child.EndToken.pos).EndToken
);

Expand Down
11 changes: 11 additions & 0 deletions Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,17 @@ method DoIt() returns (x: int) {
Assert.Single(cChildren);
}

[Fact]
public async Task DoubleComma() {
var source = @"
method Foo(a: int,, b: int) returns (x: int) {
}".TrimStart();
var documentItem = CreateTestDocument(source);
await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
var allSymbols = await RequestDocumentSymbol(documentItem);
Assert.Single(allSymbols);
}

[Fact]
public async Task LoadCorrectDocumentCreatesTopLevelSymbols() {
var source = @"
Expand Down

0 comments on commit 7d93b88

Please sign in to comment.