Fix: No more crashing on hovering bodies of nested match statements (#…

…2334)

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)

Source/Dafny/Resolver.cs

@@ -11964,7 +11964,7 @@ public RBranchStmt(IToken tok, int branchid, List<ExtendedPattern> patterns, Lis
  }
 
  public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
- this.Body = x.Body.ConvertAll((new Cloner()).CloneStmt);
+ this.Body = new List<Statement>(x.Body); // Resolving the body will insert new elements. 
  this.Attributes = attrs;
  this.Patterns.Add(x.Pat);
  }

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```]
+ }
+}");
+ }
  }
 }