diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 16ef721fc59..e000a49a97b 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,6 @@ # Upcoming +- fix: Hovering over variables and methods inside cases of nested match statements work again (https://github.com/dafny-lang/dafny/pull/2334) - fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300) - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302) - fix: Caching in the language server does not prevent gutter icons from being updated correctly. (https://github.com/dafny-lang/dafny/pull/2312) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8a565849f72..5be6687e416 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -11964,7 +11964,7 @@ public RBranchStmt(IToken tok, int branchid, List patterns, Lis } public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List()) { - this.Body = x.Body.ConvertAll((new Cloner()).CloneStmt); + this.Body = new List(x.Body); // Resolving the body will insert new elements. this.Attributes = attrs; this.Patterns.Add(x.Pat); } diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index 8943d5e3374..25266fe9bf1 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -427,5 +427,16 @@ function ToRelativeIndependent(): (p: Position) } "); } + + [TestMethod] + public async Task HoveringVariablesInsideNestedMatchStmtWorks() { + await AssertHover(@" +lemma dummy(e: int) { + match e { + case _ => var xx := 1; + ^[```dafny\nghost xx: int\n```] + } +}"); + } } }