diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 5d477b74727..84ff474ced9 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -13,6 +13,20 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; [TestClass] public class VerificationStatusTest : ClientBasedLanguageServerTest { + [TestMethod] + public async Task EmptyVerificationTaskListIsPublishedOnOpenAndChange() { + var source = "method m1() {}"; + var documentItem = CreateTestDocument(source); + await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken); + + var status1 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); + Assert.AreEqual(0, status1.NamedVerifiables.Count); + + ApplyChange(ref documentItem, new Range(0, 0, 0, 0), "\n"); + + var status2 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); + Assert.AreEqual(0, status2.NamedVerifiables.Count); + } [TestMethod] public async Task NoVerificationStatusPublishedForUnparsedDocument() { @@ -100,12 +114,9 @@ await SetUp(new Dictionary { var translatedStatusBefore = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.AreEqual(1, translatedStatusBefore.NamedVerifiables.Count); - // Delete the end of the Foo range + // Delete the end of the Foo range, so Foo() becomes F() ApplyChange(ref documentItem, new Range(0, 8, 0, 12), "()"); - var resolutionStatusAfter = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); - Assert.AreEqual(0, resolutionStatusAfter.NamedVerifiables.Count); - var translatedStatusAfter = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.AreEqual(1, translatedStatusAfter.NamedVerifiables.Count); } @@ -249,6 +260,7 @@ await SetUp(new Dictionary() { await client.SaveDocumentAndWaitAsync(documentItem, CancellationToken); + var stale2 = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); var running = await verificationStatusReceiver.AwaitNextNotificationAsync(CancellationToken); Assert.AreEqual(PublishedVerificationStatus.Running, running.NamedVerifiables[0].Status); diff --git a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs index bf2c892866a..6333d5c339a 100644 --- a/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs +++ b/Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs @@ -28,23 +28,27 @@ public void PublishNotifications(DafnyDocument previous, DafnyDocument document) } private void PublishVerificationStatus(DafnyDocument previousDocument, DafnyDocument document) { - if (!document.WasResolved) { + var notification = GetFileVerificationStatus(document); + if (notification == null) { + // Do not publish verification status while resolving return; } - var notification = GetFileVerificationStatus(document); var previous = GetFileVerificationStatus(previousDocument); - if (previous.Version > notification.Version || - previous.NamedVerifiables.SequenceEqual(notification.NamedVerifiables)) { + if (previous != null && (previous.Version > notification.Version || + previous.NamedVerifiables.SequenceEqual(notification.NamedVerifiables))) { return; } languageServer.TextDocument.SendNotification(DafnyRequestNames.VerificationSymbolStatus, notification); } - private static FileVerificationStatus GetFileVerificationStatus(DafnyDocument document) { + private static FileVerificationStatus? GetFileVerificationStatus(DafnyDocument document) { + if (document.ImplementationIdToView == null || document.VerificationTasks == null) { + return null; + } return new FileVerificationStatus(document.Uri, document.Version, - GetNamedVerifiableStatuses(document.ImplementationIdToView ?? (IReadOnlyDictionary)new Dictionary())); + GetNamedVerifiableStatuses(document.ImplementationIdToView)); } private static List GetNamedVerifiableStatuses(IReadOnlyDictionary implementationViews) {