From 2f0619ff34e2612d81f61298de1a248c7e3fcab8 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 30 Jan 2025 15:48:56 +0100
Subject: [PATCH] Fix angry module LSP diagnostic

---
 .../DafnyCore/AST/Modules/ModuleDefinition.cs |  2 +-
 .../Diagnostics/DiagnosticsTest.cs            | 20 +++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
index 65047f0d46..7582f42ae0 100644
--- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -467,7 +467,7 @@ public bool Resolve(ModuleSignature sig, ModuleResolver resolver, string exportS
         if (!nestedModuleDecl.ModuleDef.SuccessfullyResolved) {
           if (!IsEssentiallyEmptyModuleBody()) {
             // say something only if this will cause any testing to be omitted
-            resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl,
+            resolver.reporter.Error(MessageSource.Resolver, nestedModuleDecl.NameNode,
               "not resolving module '{0}' because there were errors in resolving its nested module '{1}'", Name,
               nestedModuleDecl.Name);
           }
diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
index 957ac6270d..6951416eef 100644
--- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
+++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
@@ -18,6 +18,26 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
   public class DiagnosticsTest : ClientBasedLanguageServerTest {
     private readonly string testFilesDirectory = Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles");
 
+    [Fact]
+    public async Task NestedModuleRange() {
+      var source = @"
+module A {
+  function A(x: int): int {
+    true
+  }
+  function B(x: int): int {
+    1
+  }
+}
+method Main() {
+}".TrimStart();
+      var documentItem = CreateAndOpenTestDocument(source);
+      var diagnostics1 = await GetLastDiagnostics(documentItem);
+      var startOrdered = diagnostics1.OrderBy(r => r.Range.Start).ToList();
+      Assert.Equal(new Range(0, 7, 0, 8), startOrdered[0].Range);
+      Assert.Equal(new Range(1, 2, 3, 3), startOrdered[1].Range);
+    }
+
     [Fact]
     public async Task ResolutionErrorMigration() {
       var source = @"module ResolutionError {