Use symbol name as range for timeout diagnostic

Source/DafnyCore/Verifier/Translator.BoogieFactory.cs

@@ -877,6 +877,13 @@ static Bpl.Expr BplFormalVar(string name, Bpl.Type ty, bool incoming, List<Bpl.V
     }
 
     public static IToken ToDafnyToken(Bpl.IToken exprTok) {
+      if (exprTok is BoogieRangeToken boogieRangeToken) {
+        if (boogieRangeToken.NameToken != null) {
+          return boogieRangeToken.NameToken;
+        }
+
+        return boogieRangeToken;
+      }
       if (exprTok == null) {
         return null;
       } else if (exprTok is IToken t) {

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -10,6 +10,7 @@
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Newtonsoft.Json;
+using NuGet.Frameworks;
 using Xunit.Abstractions;
 using Xunit;
 using Xunit.Sdk;
@@ -20,6 +21,15 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization {
   public class DiagnosticsTest : ClientBasedLanguageServerTest {
     private readonly string testFilesDirectory = Path.Combine(Directory.GetCurrentDirectory(), "Synchronization/TestFiles");
 
+    [Fact]
+    public async Task DiagnosticsForVerificationTimeoutHasNameAsRange() {
+      var documentItem = CreateTestDocument(SlowToVerify, "DiagnosticsForVerificationTimeout.dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+      Assert.Contains("timed out", diagnostics[0].Message);
+      Assert.Equal(new Range(0, 21, 0, 43), diagnostics[0].Range);
+    }
+
     [Fact]
     public async Task NoFlickeringWhenMixingCorrectAndErrorBatches() {
       var source = @"

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

@@ -155,7 +155,7 @@ public async Task<IEnumerable<DocumentSymbol>> RequestDocumentSymbol(TextDocumen
 
   public async Task<PublishDiagnosticsParams> GetLastDiagnosticsParams(TextDocumentItem documentItem, CancellationToken cancellationToken) {
     await client.WaitForNotificationCompletionAsync(documentItem.Uri, cancellationToken);
-    var compilation = (await Projects.GetLastDocumentAsync(documentItem))!;
+    var compilation = (await Projects.GetLastDocumentAsync(documentItem).WaitAsync(cancellationToken))!;
     Assert.NotNull(compilation);
     var expectedDiagnostics = compilation.GetDiagnostics(documentItem.Uri.ToUri()).
       Select(d => d.ToLspDiagnostic()).

Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs

@@ -133,7 +133,7 @@ method Abs(x: int) returns (y: int)
       await WaitForStatus(null, PublishedVerificationStatus.Error, CancellationToken, documentItem);
     }
 
-    [Fact(Timeout = MaxTestExecutionTimeMs)]
+    [Fact]
     public async Task DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() {
       var documentItem = CreateTestDocument(SlowToVerify, "DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);