merge origin/main

src/ast/diagnostic.rs

@@ -10,7 +10,7 @@ use std::{
 };
 
 use ariadne::{Cache, Report, ReportBuilder, ReportKind, Source};
-use lsp_types::{DiagnosticTag, VersionedTextDocumentIdentifier};
+use lsp_types::{DiagnosticTag, TextDocumentIdentifier, VersionedTextDocumentIdentifier};
 use pathdiff::diff_paths;
 
 use crate::pretty::{Doc, SimplePretty};
@@ -157,6 +157,13 @@ impl Files {
         self.files.iter().find(|file| &file.path == path)
     }
 
+    pub fn find_uri(&self, document_id: TextDocumentIdentifier) -> Option<&Arc<StoredFile>> {
+        self.files.iter().find(|file| match &file.path {
+            SourceFilePath::Lsp(ident) => ident.uri == document_id.uri,
+            _ => false,
+        })
+    }
+
     pub fn char_span(&self, span: Span) -> CharSpan {
         self.get(span.file).unwrap().char_span(span)
     }

src/servers/lsp.rs

@@ -129,7 +129,8 @@ impl LspServer {
                             })
                             .id;
                         drop(files);
-                        self.clear_all().map_err(VerifyError::ServerError)?;
+                        self.clear_file_information(&file_id)
+                            .map_err(VerifyError::ServerError)?;
                         let result = verify(self, &[file_id]);
                         let res = match &result {
                             Ok(_) => Response::new_ok(id, Value::Null),
@@ -195,9 +196,22 @@ impl LspServer {
                 Ok(None)
             }
             "textDocument/didClose" => {
-                let _params: DidCloseTextDocumentParams =
+                let params: DidCloseTextDocumentParams =
                     notification.extract("textDocument/didClose")?;
-                // TODO: remove file?
+
+                let file_id = self
+                    .files
+                    .lock()
+                    .unwrap()
+                    .find_uri(params.text_document.clone())
+                    .unwrap_or_else(|| {
+                        panic!(
+                            "Could not find file id for document {:?}",
+                            params.text_document
+                        )
+                    })
+                    .id;
+                self.clear_file_information(&file_id)?;
                 Ok(None)
             }
             _ => Ok(Some(notification)),
@@ -297,14 +311,14 @@ impl LspServer {
         Ok(())
     }
 
-    fn clear_all(&mut self) -> Result<(), ServerError> {
-        for diags in self.diagnostics.values_mut() {
-            diags.clear();
+    fn clear_file_information(&mut self, file_id: &FileId) -> Result<(), ServerError> {
+        if let Some(diag) = self.diagnostics.get_mut(file_id) {
+            diag.clear();
         }
-        for explanations in self.vc_explanations.values_mut() {
+        if let Some(explanations) = self.vc_explanations.get_mut(file_id) {
             explanations.clear();
         }
-        self.statuses.clear();
+        self.statuses.retain(|span, _| span.file != *file_id);
         self.publish_diagnostics()?;
         self.publish_verify_statuses()?;
         Ok(())

vscode-ext/src/CaesarClient.ts

@@ -13,12 +13,12 @@ import { WalkthroughComponent } from "./WalkthroughComponent";
 import Logger from "./Logger";
 
 export enum ServerStatus {
+    NotStarted,
     Stopped,
     Starting,
     Ready,
     FailedToStart,
     Verifying,
-    Finished
 }
 
 export enum VerifyResult {
@@ -398,7 +398,7 @@ export class CaesarClient {
         this.notifyStatusUpdate(ServerStatus.Verifying);
         try {
             await this.client.sendRequest('custom/verify', { text_document: documentItem });
-            this.notifyStatusUpdate(ServerStatus.Finished);
+            this.notifyStatusUpdate(ServerStatus.Ready);
             this.logger.info("Client: completed verification.", document.uri);
             await this.walkthrough.setVerifiedHeyVL(true);
         } catch (error) {

vscode-ext/src/ComputedPreComponent.ts

@@ -56,6 +56,12 @@ export class ComputedPreComponent {
             }
         }));
 
+        verifier.context.subscriptions.push(vscode.workspace.onDidCloseTextDocument((document) => {
+            const documentIdentifier = { uri: document.uri.toString() };
+            this.computedPres.remove(documentIdentifier);
+            this.render();
+        }));
+
         // listen to custom/computedPre notifications
         verifier.client.onComputedPre((update) => {
             this.computedPres.insert(update.document, update.pres);
@@ -64,14 +70,16 @@ export class ComputedPreComponent {
 
         // clear all information when a new verification task is started
         verifier.client.onStatusUpdate((status) => {
-            if (status !== ServerStatus.Finished) {
+            if (status == ServerStatus.Verifying) {
                 for (const [_document, results] of this.computedPres.entries()) {
                     results.length = 0;
                 }
                 this.render();
             }
         });
 
+
+
         // TODO: listen to content changes to remove lines?
     }
 

vscode-ext/src/GutterStatusComponent.ts

@@ -4,6 +4,7 @@ import { GutterInformationViewConfig } from "./Config";
 import { ServerStatus, VerifyResult } from "./CaesarClient";
 import { DocumentMap, Verifier } from "./Verifier";
 import { ConfigurationConstants } from "./constants";
+import { TextDocumentIdentifier } from "vscode-languageclient";
 
 export class GutterStatusComponent {
 
@@ -40,7 +41,7 @@ export class GutterStatusComponent {
 
         // listen to status and verify updates
         verifier.client.onStatusUpdate((status) => {
-            if (status !== ServerStatus.Finished) {
+            if (status == ServerStatus.Verifying) {
                 for (const [_document, results] of this.status.entries()) {
                     results.length = 0;
                 }
@@ -52,6 +53,12 @@ export class GutterStatusComponent {
             this.status.insert(document, results);
             this.render();
         });
+
+        verifier.context.subscriptions.push(vscode.workspace.onDidCloseTextDocument((document) => {
+            const documentIdentifier: TextDocumentIdentifier = { uri: document.uri.toString() };
+            this.status.remove(documentIdentifier);
+            this.render();
+        }));
     }
 
     render() {

vscode-ext/src/StatusBarComponent.ts

@@ -1,14 +1,27 @@
-import { StatusBarItem } from "vscode";
+import { StatusBarItem, Range } from "vscode";
 import * as vscode from 'vscode';
 import { StatusBarViewConfig } from "./Config";
-import { ServerStatus } from "./CaesarClient";
-import { Verifier } from "./Verifier";
+import { ServerStatus, VerifyResult } from "./CaesarClient";
+import { DocumentMap, Verifier } from "./Verifier";
 import { ConfigurationConstants } from "./constants";
+import { TextDocumentIdentifier } from "vscode-languageclient";
+
+
+const runningTooltipMenu =
+    new vscode.MarkdownString(
+        "[Stop Caesar](command:caesar.stopServer)\n\n" +
+        "[Restart Caesar](command:caesar.restartServer)"
+        , true);
+
+const stoppedTooltipMenu =
+    new vscode.MarkdownString(
+        "[Start Caesar](command:caesar.startServer)", true);
 
 export class StatusBarComponent {
 
     private enabled: boolean;
-    private status: ServerStatus = ServerStatus.Stopped;
+    private verifyStatus: DocumentMap<[Range, VerifyResult][]> = new DocumentMap();
+    private serverStatus: ServerStatus = ServerStatus.NotStarted;
     private view: StatusBarItem;
 
     constructor(verifier: Verifier) {
@@ -18,11 +31,6 @@ export class StatusBarComponent {
         this.view.text = "Caesar";
         this.view.command = "caesar.showOutput";
 
-        this.view.tooltip = new vscode.MarkdownString(
-            "[Restart Caesar](command:caesar.restartServer)\n\n" +
-            "[Start Caesar](command:caesar.startServer)\n\n" +
-            "[Stop Caesar](command:caesar.stopServer)",
-            true);
 
         // render if enabled
         this.enabled = StatusBarViewConfig.get(ConfigurationConstants.showStatusBar);
@@ -38,36 +46,161 @@ export class StatusBarComponent {
 
         // listen to verifier updates
         verifier.client.onStatusUpdate((status) => {
-            this.status = status;
+            this.serverStatus = status;
             this.render();
         });
+
+        verifier.client.onVerifyResult((document, results) => {
+            this.verifyStatus.insert(document, results);
+            this.render();
+        });
+
+        verifier.context.subscriptions.push(vscode.workspace.onDidCloseTextDocument((document) => {
+            const documentIdentifier: TextDocumentIdentifier = { uri: document.uri.toString() };
+            this.verifyStatus.remove(documentIdentifier);
+            this.render();
+        }));
+
+        verifier.context.subscriptions.push(vscode.window.onDidChangeVisibleTextEditors(() => {
+            this.render();
+        }));
+
+        verifier.context.subscriptions.push(vscode.workspace.onDidOpenTextDocument(() => {
+            this.render();
+        }));
     }
 
     render() {
+        let viewText = "";
+        let command = "";
+        let tooltipMenuText = new vscode.MarkdownString();
+        let tooltipStatusText = new vscode.MarkdownString();
         if (this.enabled) {
-            switch (this.status) {
+
+            switch (this.serverStatus) {
+                case ServerStatus.NotStarted:
+                    viewText = "$(debug-start) Caesar Inactive";
+                    command = "caesar.startServer";
+                    tooltipMenuText = stoppedTooltipMenu;
+                    break;
                 case ServerStatus.Stopped:
-                    this.view.text = "$(debug-stop) Et tu, Brute?";
+                    viewText = "$(debug-start) Et tu, Brute?";
+                    command = "caesar.startServer";
+                    tooltipMenuText = stoppedTooltipMenu;
                     break;
                 case ServerStatus.FailedToStart:
-                    this.view.text = "$(warning) Failed to start Caesar";
+                    viewText = "$(warning) Failed to start Caesar";
+                    command = "caesar.startServer";
+                    tooltipMenuText = stoppedTooltipMenu;
                     break;
                 case ServerStatus.Starting:
-                    this.view.text = "$(sync~spin) Starting Caesar...";
+                    viewText = "$(loading~spin) Starting Caesar...";
+                    command = "caesar.showOutput"
                     break;
                 case ServerStatus.Ready:
-                    this.view.text = "$(check) Caesar Ready";
+                    [viewText, tooltipStatusText] = this.getReadyStatusView();
+                    command = "caesar.showOutput";
+                    tooltipMenuText = runningTooltipMenu;
                     break;
                 case ServerStatus.Verifying:
-                    this.view.text = "$(sync~spin) Verifying...";
-                    break;
-                case ServerStatus.Finished:
-                    this.view.text = "$(check) Verified";
+                    viewText = "$(sync~spin) Verifying...";
+                    command = "caesar.showOutput"
                     break;
             }
+
+            this.view.text = viewText;
+            this.view.command = command;
+            this.renderTooltip(tooltipMenuText, tooltipStatusText);
             this.view.show();
         } else {
             this.view.hide();
         }
     }
+
+    /// Renders the tooltip by combining the given menu and status text.
+    private renderTooltip(tooltipMenuText: vscode.MarkdownString, tooltipStatusText: vscode.MarkdownString) {
+        if (tooltipStatusText.value === "") {
+            this.view.tooltip = tooltipMenuText;
+            this.view.tooltip.isTrusted = true;
+            return;
+        }
+        this.view.tooltip = new vscode.MarkdownString(tooltipMenuText.value + "\n\n --- \n" + tooltipStatusText.value, true);
+        this.view.tooltip.isTrusted = true;
+    }
+
+
+    /// Returns the status view text and tooltip for the ready status by aggregating the verification results for each visible editor.
+    private getReadyStatusView(): [string, vscode.MarkdownString] {
+        let viewText = "";
+        let tooltipString = new vscode.MarkdownString("", true);
+
+        let someError = false;
+        let someVerified = false;
+
+        const editorsWithResults = vscode.window.visibleTextEditors.filter((editor) => {
+            return (this.verifyStatus.get({ uri: editor.document.uri.toString() }) ?? []).length !== 0; // And only files with results
+        });
+
+        if (editorsWithResults.length === 0) {
+            return ["$(thumbsup-filled) Caesar Ready", new vscode.MarkdownString("Verify some HeyVL files!", true)];
+        }
+
+        for (const editor of editorsWithResults) {
+            const document_id: TextDocumentIdentifier = { uri: editor.document.uri.toString() };
+
+            const results = this.verifyStatus.get(document_id);
+
+            if (results === undefined) throw new Error("No verify results found for document: " + document_id);
+
+            let verified = 0;
+            let failed = 0;
+            let unknown = 0;
+
+            for (const [_, result] of results) {
+                switch (result) {
+                    case VerifyResult.Verified:
+                        verified++;
+                        break;
+                    case VerifyResult.Failed:
+                        failed++;
+                        break;
+                    case VerifyResult.Unknown:
+                        unknown++;
+                        break;
+                }
+            }
+
+            if (failed > 0 || unknown > 0) {
+                someError = true;
+            }
+            if (verified > 0) {
+                someVerified = true;
+            }
+
+            tooltipString.appendMarkdown(`${vscode.Uri.parse(document_id.uri).path}: $(error) ${failed} $(question) ${unknown}` + "\n\n --- \n");
+        }
+
+        // Remove the last newline and separator
+        tooltipString.value.trimEnd();
+
+        if (!someError && someVerified) {
+            // No error and at least one verified implies everything is verified.
+            viewText = "$(pass) Verified!";
+            tooltipString = new vscode.MarkdownString("No errors found", true);
+        } else if (someError) {
+            // At least one verified, but some errors
+            viewText = "$(warning) Verification Errors";
+        } else if (!someError && !someVerified) {
+            // No error and no verified implies the file is either empty or there are syntax errors.
+            viewText = "$(error) Invalid File";
+            tooltipString = new vscode.MarkdownString("Syntax error or empty file!", true);
+        }
+
+        return [viewText, tooltipString];
+
+    }
+
 }
+
+
+

vscode-ext/src/Verifier.ts

@@ -27,6 +27,10 @@ export class DocumentMap<T> {
     public entries(): [TextDocumentIdentifier, T][] {
         return Array.from(this.map.values());
     }
+
+    public remove(document_id: TextDocumentIdentifier) {
+        this.map.delete(document_id.uri.toString());
+    }
 }
 
 export class Verifier {