diff --git a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
index e451437e480..39a216cc1f7 100644
--- a/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
+++ b/Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs
@@ -46,13 +46,13 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ParsingFailed);
 
       // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued.
       var otherDoc = CreateTestDocument(source, "Test2.dfy");
       client.OpenDocument(otherDoc);
-      await AssertProgress(otherDoc, CompilationStatus.ResolutionStarted);
+      await AssertProgress(otherDoc, CompilationStatus.Parsing);
       await AssertProgress(otherDoc, CompilationStatus.ParsingFailed);
     }
 
@@ -67,12 +67,14 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.ResolutionFailed);
 
       // We re-send the same erroneous document again to check that we don't have a CompilationSucceeded event queued.
       var otherDoc = CreateTestDocument(source, "Test2.dfy");
       client.OpenDocument(otherDoc);
+      await AssertProgress(otherDoc, CompilationStatus.Parsing);
       await AssertProgress(otherDoc, CompilationStatus.ResolutionStarted);
       await AssertProgress(otherDoc, CompilationStatus.ResolutionFailed);
     }
@@ -91,6 +93,7 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
     }
@@ -115,6 +118,7 @@ method Abs(x: int) returns (y: int)
 ".TrimStart();
       var documentItem = CreateTestDocument(source);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
     }
@@ -123,6 +127,7 @@ method Abs(x: int) returns (y: int)
     public async Task DocumentWithOnlyCodedVerifierTimeoutSendsCompilationSucceededVerificationStartedAndVerificationFailedStatuses() {
       var documentItem = CreateTestDocument(SlowToVerify);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
     }
@@ -132,6 +137,7 @@ public async Task DocumentWithOnlyConfiguredVerifierTimeoutSendsCompilationSucce
       await SetUp(options => options.Set(BoogieOptionBag.VerificationTimeLimit, 3U));
       var documentItem = CreateTestDocument(SlowToVerify);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem, CompilationStatus.CompilationSucceeded);
     }
@@ -151,13 +157,16 @@ method Abs(x: int) returns (y: int)
       // compilation status twice without any verification status inbetween.
       var documentItem1 = CreateTestDocument(source, "test_1.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
-      var documentItem2 = CreateTestDocument(source, "test_2dfy");
-      await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
-
+      await AssertProgress(documentItem1, CompilationStatus.Parsing);
       await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded);
+      await AssertProgress(documentItem1, CompilationStatus.PreparingVerification);
+      var documentItem2 = CreateTestDocument(source, "test_2dfy");
+      await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
+      await AssertProgress(documentItem2, CompilationStatus.Parsing);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded);
+      await AssertProgress(documentItem2, CompilationStatus.PreparingVerification);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -176,13 +185,17 @@ method Abs(x: int) returns (y: int)
       var documentItem1 = CreateTestDocument(source, "test_1.dfy");
       await client.OpenDocumentAndWaitAsync(documentItem1, CancellationToken);
       await client.SaveDocumentAndWaitAsync(documentItem1, CancellationToken);
+      await AssertProgress(documentItem1, CompilationStatus.Parsing);
+      await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
+      await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded);
+      await AssertProgress(documentItem1, CompilationStatus.PreparingVerification);
       var documentItem2 = CreateTestDocument(source, "test_2dfy");
       await client.OpenDocumentAndWaitAsync(documentItem2, CancellationToken);
       await client.SaveDocumentAndWaitAsync(documentItem2, CancellationToken);
-      await AssertProgress(documentItem1, CompilationStatus.ResolutionStarted);
-      await AssertProgress(documentItem1, CompilationStatus.CompilationSucceeded);
+      await AssertProgress(documentItem2, CompilationStatus.Parsing);
       await AssertProgress(documentItem2, CompilationStatus.ResolutionStarted);
       await AssertProgress(documentItem2, CompilationStatus.CompilationSucceeded);
+      await AssertProgress(documentItem2, CompilationStatus.PreparingVerification);
     }
 
     [Fact(Timeout = MaxTestExecutionTimeMs)]
@@ -196,7 +209,7 @@ lemma Something(i: int)
     }";
       var documentItem = CreateTestDocument(source);
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
-      await AssertProgress(documentItem, CompilationStatus.ResolutionStarted);
+      await AssertProgress(documentItem, CompilationStatus.Parsing);
       await AssertProgress(documentItem, CompilationStatus.ParsingFailed);
     }
 
diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs
index 0529b693c62..42194d64e95 100644
--- a/Source/DafnyLanguageServer/Workspace/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs
@@ -133,6 +133,8 @@ public async Task<DocumentAfterTranslation> PrepareVerificationTasksAsync(
       throw new TaskCanceledException();
     }
 
+    statusPublisher.SendStatusNotification(loaded.TextDocumentItem, CompilationStatus.PreparingVerification);
+
     var verificationTasks =
       await verifier.GetVerificationTasksAsync(loaded, cancellationToken);
 
diff --git a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs b/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs
deleted file mode 100644
index 5f282702bb0..00000000000
--- a/Source/DafnyLanguageServer/Workspace/DafnyDocument.cs
+++ /dev/null
@@ -1 +0,0 @@
-
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs b/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs
index d1540611cd7..ad237ae69d2 100644
--- a/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs
+++ b/Source/DafnyLanguageServer/Workspace/Notifications/CompilationStatus.cs
@@ -7,9 +7,11 @@ namespace Microsoft.Dafny.LanguageServer.Workspace.Notifications {
   /// </summary>
   [JsonConverter(typeof(StringEnumConverter))]
   public enum CompilationStatus {
-    ResolutionStarted,
+    Parsing,
     ParsingFailed,
+    ResolutionStarted,
     ResolutionFailed,
+    PreparingVerification,
     CompilationSucceeded
   }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index ee70d061f4e..e0d26389fc2 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -84,7 +84,7 @@ private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuff
       CancellationToken cancellationToken) {
       var outerModule = new DefaultModuleDefinition(new List<Uri>() { textDocument.Uri.ToUri() });
       var errorReporter = new DiagnosticErrorReporter(options, outerModule, textDocument.Text, textDocument.Uri);
-      statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
+      statusPublisher.SendStatusNotification(textDocument, CompilationStatus.Parsing);
       var program = parser.Parse(textDocument, errorReporter, cancellationToken);
       var documentAfterParsing = new DocumentAfterParsing(textDocument, program, errorReporter.GetDiagnostics(textDocument.Uri));
       if (errorReporter.HasErrors) {
@@ -92,6 +92,7 @@ private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuff
         return documentAfterParsing;
       }
 
+      statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
       var compilationUnit = symbolResolver.ResolveSymbols(textDocument, program, out _, cancellationToken);
       var symbolTable = symbolTableFactory.CreateFrom(compilationUnit, cancellationToken);
 
diff --git a/docs/dev/news/4031.feat b/docs/dev/news/4031.feat
new file mode 100644
index 00000000000..2add8f39f93
--- /dev/null
+++ b/docs/dev/news/4031.feat
@@ -0,0 +1 @@
+Allow the Dafny IDE to publish 'Parsing' and 'Preparing Verification' messages to let the user better understand what they're waiting for.
\ No newline at end of file