From fb4b98afffe8e4216a757d979edfd827b70aca50 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 12 May 2022 13:51:30 -0500
Subject: [PATCH] Fixed the rebase

---
 .../DafnyLanguageServer/Handlers/DafnyHoverHandler.cs |  1 +
 .../Workspace/TextDocumentLoader.cs                   |  1 -
 .../Workspace/VerificationProgressReporter.cs         | 11 +++++++++--
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
index 831e40fcd62..cc5c8694edd 100644
--- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs
@@ -12,6 +12,7 @@
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using VerificationStatus = Microsoft.Dafny.LanguageServer.Workspace.Notifications.VerificationStatus;
 
 namespace Microsoft.Dafny.LanguageServer.Handlers {
   public class DafnyHoverHandler : HoverHandlerBase {
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index f712952f2ec..6e34aa2c780 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -195,7 +195,6 @@ public IObservable<DafnyDocument> Verify(DafnyDocument document, CancellationTok
         var outcomeError = result.GetOutcomeError(Options);
         if (outcomeError != null) {
           errorReporter.ReportBoogieError(outcomeError);
-          methodTree.ResourceCount = 0;
         }
 
         var diagnostics = errorReporter.GetDiagnostics(document.Uri).OrderBy(d => d.Range.Start).ToList();
diff --git a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
index f77cbcba195..b0afd412ba1 100644
--- a/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
+++ b/Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs
@@ -202,6 +202,7 @@ public void ReportRealtimeDiagnostics(bool verificationStarted, DafnyDocument? d
   private void ReportMethodsBeingVerified(string extra = "") {
     var pending = document.VerificationTree.Children
       .Where(diagnostic => diagnostic.Started && !diagnostic.Finished)
+      .OrderBy(diagnostic => diagnostic.StartTime)
       .Select(diagnostic => diagnostic.DisplayName)
       .ToList();
     var total = document.VerificationTree.Children.Count();
@@ -259,6 +260,8 @@ public void ReportEndVerifyImplementation(Implementation implementation, Verific
     } else {
       lock (LockProcessing) {
         implementationNode.Stop();
+        implementationNode.ResourceCount = verificationResult.ResourceCount;
+        targetMethodNode.ResourceCount += verificationResult.ResourceCount;
         var finalOutcome = verificationResult.Outcome switch {
           ConditionGeneration.Outcome.Correct => VerificationStatus.Verified,
           _ => VerificationStatus.Error
@@ -307,7 +310,10 @@ public void ReportAssertionBatchResult(Split split,
         result.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExample);
 
         var assertionBatchIndex = implementationNode.GetNewAssertionBatchCount();
-        implementationNode.IncreaseNewAssertionBatchCount();
+        var assertionBatchTime = (int)result.runTime.TotalMilliseconds;
+        var assertionBatchResourceCount = result.resourceCount;
+        implementationNode.AddAssertionBatchTime(assertionBatchTime);
+        implementationNode.AddAssertionBatchResourceCount(assertionBatchResourceCount);
 
         // Attaches the trace
         void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken token,
@@ -337,7 +343,8 @@ void AddChildOutcome(Counterexample? counterexample, AssertCmd assertCmd, IToken
             AssertionBatchIndex = assertionBatchIndex,
             Started = true,
             Finished = true
-          }.WithAssertionAndCounterExample(assertCmd, counterexample);
+          }.WithDuration(implementationNode.StartTime, assertionBatchTime)
+            .WithAssertionAndCounterExample(assertCmd, counterexample);
           // Add this diagnostics as the new one to display once the implementation is fully verified
           implementationNode.AddNewChild(nodeDiagnostic);
           // Update any previous pending "verifying" diagnostic as well so that they are updated in real-time