Merge pull request #35 from DafnyVSCode/feature/status-messages

Update status message handling

Author: camrein

CHANGELOG.md

@@ -6,7 +6,7 @@
 
 ## 1.7.0
 
-- Now changing status to *Not Verified* as soon as a document is edited.
+- Now showing parser and resolver errors in the status bar.
 
 ## 1.6.0
 

src/stringResources/languageServer.ts

@@ -21,10 +21,24 @@ export class LanguageServerNotification {
   public static DafnyLanguageServerVersionReceived: string =
     "dafnyLanguageServerVersionReceived";
 
+  public static CompilationStatus: string = "dafny/compilation/status";
+  // TODO: Status messages for Dafny 3.2, remove in the future.
   public static VerificationStarted: string = "dafny/verification/started";
   public static VerificationCompleted: string = "dafny/verification/completed";
 }
 
+/**
+ * Statuses sent by the language server while processing a document.
+ */
+export enum CompilationStatus {
+  ParsingFailed = "ParsingFailed",
+  ResolutionFailed = "ResolutionFailed",
+  CompilationSucceeded = "CompilationSucceeded",
+  VerificationStarted = "VerificationStarted",
+  VerificationFailed = "VerificationFailed",
+  VerificationSucceeded = "VerificationSucceeded"
+}
+
 /**
  * Configuration settings for the Dafny language server
  * These settings are mostly no longer necessary

src/stringResources/messages.ts

@@ -60,13 +60,20 @@ export class Information {
 }
 
 export class StatusbarStrings {
-  public static Verified: string = "$(thumbsup) Verified";
-  public static NotVerified: string = "$(thumbsdown) Not verified";
+  public static ParsingFailed: string = "$(thumbsdown) Parsing Failed";
+  public static ResolutionFailed: string = "$(thumbsdown) Resolution Failed";
+  public static CompilationSucceeded: string = "$(thumbsup) Compilation Succeeded";
   public static Verifying: string = "$(sync~spin) Verifying...";
+  public static VerificationSucceeded: string = "$(thumbsup) Verification Succeeded";
+  public static VerificationFailed: string = "$(thumbsdown) Not verified";
   public static Errors: string = "Errors";
   public static Pending: string = "$(issue-opened) Server answer pending";
   public static DafnyVersion: string = "DafnyLS";
   public static CurrentDocument: string = "Current Document";
   public static NoDocumentSelected: string = "No document selected yet.";
   public static Started: string = "Server started";
+  
+  // TODO: Status messages for Dafny 3.2, remove in the future.
+  public static Verified: string = "$(thumbsup) Verified";
+  public static NotVerified: string = StatusbarStrings.VerificationFailed;
 }

src/ui/providers/statusbarProvider.ts

@@ -1,12 +1,12 @@
 "use strict";
 import {
   window,
-  workspace,
   Uri,
   StatusBarItem,
   StatusBarAlignment,
   LanguageClient,
 } from "../../ideApi/_IdeApi";
+import { CompilationStatus } from "../../stringResources/languageServer";
 import {
   LanguageServerNotification,
   StatusbarStrings,
@@ -15,6 +15,15 @@ import {
 
 import { IStatusbarProvider } from "./IStatusbarProvider";
 
+const COMPILATION_STATUS_MESSAGE_MAPPINGS = {
+  [CompilationStatus.ParsingFailed]: StatusbarStrings.ParsingFailed,
+  [CompilationStatus.ResolutionFailed]: StatusbarStrings.ResolutionFailed,
+  [CompilationStatus.CompilationSucceeded]: StatusbarStrings.CompilationSucceeded,
+  [CompilationStatus.VerificationStarted]: StatusbarStrings.Verifying,
+  [CompilationStatus.VerificationSucceeded]: StatusbarStrings.VerificationSucceeded,
+  [CompilationStatus.VerificationFailed]: StatusbarStrings.VerificationFailed
+};
+
 /**
  * This component adds additional information to the status bar like
  * if the Dafny file is valid or not and how many errors were found.
@@ -46,6 +55,17 @@ export class StatusbarProvider implements IStatusbarProvider {
       }
     );
 
+    // Sent when there are any changes to the compilation status of a document.
+    languageServer.onNotification(
+      LanguageServerNotification.CompilationStatus,
+      ({ uri, status }: { uri: string, status: CompilationStatus }) => {
+        this.verificationMessage[Uri.parse(uri).toString()] =
+          COMPILATION_STATUS_MESSAGE_MAPPINGS[status];
+        this.update();
+      }
+    );
+
+    // TODO: Status message for Dafny 3.2, remove in the future.
     // Sent when the verification of a document started
     languageServer.onNotification(
       LanguageServerNotification.VerificationStarted,
@@ -55,7 +75,8 @@ export class StatusbarProvider implements IStatusbarProvider {
         this.update();
       }
     );
-
+    
+    // TODO: Status messages for Dafny 3.2, remove in the future.
     // Sent when the verification of a document completed
     languageServer.onNotification(
       LanguageServerNotification.VerificationCompleted,
@@ -66,10 +87,6 @@ export class StatusbarProvider implements IStatusbarProvider {
         this.update();
       }
     );
-
-    workspace.onDidChangeTextDocument(event => {
-      this.verificationMessage[event.document.uri.toString()] = StatusbarStrings.NotVerified;
-    });
   }
 
   public dispose(): void {