Skip to content

Commit

Permalink
Fix: Top-level symbols are now all verified. (#4443)
Browse files Browse the repository at this point in the history
Fixes #4442
In #4427, a bug was introduced
which prevent multiple top-level verification symbols to be reported,
only the first one would. This adds a test to cover the issue and fixes
it. I verified that the test was failing before the fix, and now the
test is passing. I am not adding a docs/dev/news entry because the bug
was introduced after the 4.2.0 release.

<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->

<!-- Is this a bug fix? Remember to include a test in Test/git-issues/
-->

<!-- Is this a bug fix for an issue introduced in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

<!-- Does this PR need tests? Add them to `Test/` or to
`Source/*.Test/…` and run them with `dotnet test` -->

<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to
learn how to do that while maintaining git history -->

<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
MikaelMayer authored and keyboardDrummer committed Sep 19, 2023
1 parent 084ee8b commit f5c0c9e
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 9 deletions.
11 changes: 2 additions & 9 deletions Source/DafnyCore/Generic/NodeExtensions.cs
Original file line number Diff line number Diff line change
Expand Up @@ -115,18 +115,11 @@ public static IEnumerable<LList<INode>> FindNodeChainsInUri(this INode node, Uri
return new[] { new LList<INode>(node, parent) };
}

return null;
return new LList<INode>[] { };
}

var newParent = new LList<INode>(node, parent);
foreach (var child in node.Children) {
var result = child.FindNodeChainsInUri(uri, newParent);
if (result != null) {
return result;
}
}

return null;
return node.Children.SelectMany(child => child.FindNodeChainsInUri(uri, newParent));
}

private static LList<INode> FindNodeChain(this INode node, Uri uri, DafnyPosition position, LList<INode> parent,
Expand Down
16 changes: 16 additions & 0 deletions Source/DafnyLanguageServer.Test/Lookup/DocumentSymbolTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,22 @@ method DoIt() returns (x: int) {
Assert.Single(cChildren);
}

[Fact]
public async Task LoadCorrectDocumentCreatesTopLevelSymbols() {
var source = @"
method DoIt() returns (x: int) {
}
method CallIt() returns () {
var x := DoIt();
}".TrimStart();
var documentItem = CreateTestDocument(source);
await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
var allSymbols = await RequestDocumentSymbol(documentItem);
Assert.Equal(2, allSymbols.Count());
}


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

0 comments on commit f5c0c9e

Please sign in to comment.