Show commands in tooltip (closes #223)

viperproject · Aug 8, 2023 · f93022f · f93022f
1 parent 364da87
commit f93022f
Show file tree

Hide file tree

Showing 5 changed files with 45 additions and 27 deletions.
diff --git a/package.json b/package.json
@@ -2,7 +2,7 @@
 	"name": "prusti-assistant",
 	"displayName": "Prusti Assistant",
 	"description": "Verify Rust programs with the Prusti verifier.",
-	"version": "0.12.0",
+	"version": "0.12.1",
 	"publisher": "viper-admin",
 	"repository": {
 		"type": "git",

diff --git a/src/diagnostics.ts b/src/diagnostics.ts
@@ -562,13 +562,11 @@ export class DiagnosticsManager {
     private target: vscode.DiagnosticCollection;
     private procDestructors: Set<util.KillFunction> = new Set();
     private verificationStatus: vscode.StatusBarItem;
-    private killAllButton: vscode.StatusBarItem;
     private runCount = 0;
 
-    public constructor(target: vscode.DiagnosticCollection, verificationStatus: vscode.StatusBarItem, killAllButton: vscode.StatusBarItem) {
+    public constructor(target: vscode.DiagnosticCollection, verificationStatus: vscode.StatusBarItem) {
         this.target = target;
         this.verificationStatus = verificationStatus;
-        this.killAllButton = killAllButton;
     }
 
     public dispose(): void {
@@ -591,17 +589,18 @@ export class DiagnosticsManager {
         const currentRun = this.runCount;
         util.log(`Preparing verification run #${currentRun}.`);
         this.killAll();
-        this.killAllButton.show();
 
         // Run verification
         const escapedFileName = path.basename(targetPath).replace("$", "\\$");
         this.verificationStatus.text = `$(sync~spin) Verifying ${target} '${escapedFileName}'...`;
+        this.verificationStatus.tooltip = "Status of the Prusti verification. Click to stop Prusti.";
+        this.verificationStatus.command = "prusti-assistant.killAll";
 
         const verificationDiagnostics = new VerificationDiagnostics();
         let durationSecMsg: string | null = null;
         const crashErrorMsg = "Prusti encountered an unexpected error. " +
-            "We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). " +
-            "See the log (View -> Output -> Prusti Assistant) for more details.";
+            "If the issue persists, please open a [bug report](https://github.com/viperproject/prusti-dev/issues/new). " +
+            "See [the logs](command:prusti-assistant.openLogs) for more details.";
         let crashed = false;
         try {
             let diagnostics: Diagnostic[], status: VerificationStatus, duration: util.Duration;
@@ -633,11 +632,10 @@ export class DiagnosticsManager {
             util.log(`Discarding the result of the verification run #${currentRun}, because the latest is #${this.runCount}.`);
         } else {
             // Render diagnostics
-            this.killAllButton.hide();
             verificationDiagnostics.renderIn(this.target);
             if (crashed) {
                 this.verificationStatus.text = `$(error) Verification of ${target} '${escapedFileName}' failed with an unexpected error`;
-                this.verificationStatus.command = "workbench.action.output.toggleOutput";
+                this.verificationStatus.command = "prusti-assistant.openLogs";
             } else if (verificationDiagnostics.hasErrors()) {
                 const counts = verificationDiagnostics.countsBySeverity();
                 const errors = counts.get(vscode.DiagnosticSeverity.Error);
@@ -654,6 +652,7 @@ export class DiagnosticsManager {
                 this.verificationStatus.text = `$(check) Verification of ${target} '${escapedFileName}' succeeded (${durationSecMsg} s)`;
                 this.verificationStatus.command = undefined;
             }
+            this.verificationStatus.tooltip = "Status of the Prusti verification.";
         }
     }
 }
diff --git a/src/extension.ts b/src/extension.ts
@@ -12,7 +12,18 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
     const showVersionCommand = "prusti-assistant.show-version";
     const verifyProgramCommand = "prusti-assistant.verify";
     const killAllCommand = "prusti-assistant.killAll";
+    const openLogsCommand = "prusti-assistant.openLogs";
+    const openServerLogsCommand = "prusti-assistant.openServerLogs";
     const updateCommand = "prusti-assistant.update";
+    const restartServerCommand = "prusti-assistant.restart-server";
+
+    // Open logs on command
+    context.subscriptions.push(
+        vscode.commands.registerCommand(openLogsCommand, () => util.showLogs())
+    );
+    context.subscriptions.push(
+        vscode.commands.registerCommand(openServerLogsCommand, () => server.showLogs())
+    );
 
     // Verification status
     const verificationStatus = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 10);
@@ -87,24 +98,26 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
     );
 
     // Verify on click
-    const verifyProgramButton = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 12);
-    verifyProgramButton.command = verifyProgramCommand;
-    verifyProgramButton.text = "$(play) Verify with Prusti";
-    verifyProgramButton.tooltip = "Run the Prusti verifier on this file.";
-    verifyProgramButton.show();
-    context.subscriptions.push(verifyProgramButton);
-
-    // Kill-all on click
-    const killAllButton = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 11);
-    killAllButton.command = killAllCommand;
-    killAllButton.text = "$(close) Stop Prusti";
-    killAllButton.tooltip = "Kill all Prusti processes.";
-    killAllButton.command = killAllCommand;
-    context.subscriptions.push(killAllButton);
+    const prustiButton = vscode.window.createStatusBarItem(vscode.StatusBarAlignment.Left, 11);
+    prustiButton.command = verifyProgramCommand;
+    prustiButton.text = "$(play) Prusti";
+    prustiButton.tooltip = new vscode.MarkdownString(
+        "Run the [Prusti verifier](http://prusti.org) on the current file.\n\n" +
+        "---\n\n" +
+        "$(link) [User guide](https://viperproject.github.io/prusti-dev/user-guide/)\n\n" +
+        "$(link) [Zulip chat](https://prusti.zulipchat.com/)\n\n" +
+        `[Show version](command:${showVersionCommand})\n\n` +
+        `[Update Prusti](command:${updateCommand})\n\n` +
+        `[Restart server](command:${restartServerCommand})`,
+        true,
+    );
+    prustiButton.tooltip.isTrusted = true;
+    prustiButton.show();
+    context.subscriptions.push(prustiButton);
 
     // Restart the server on command
     context.subscriptions.push(
-        vscode.commands.registerCommand("prusti-assistant.restart-server", async () => {
+        vscode.commands.registerCommand(restartServerCommand, async () => {
             await server.restart(context, verificationStatus);
         })
     );
@@ -143,7 +156,6 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
     const verificationManager = new diagnostics.DiagnosticsManager(
         verificationDiagnostics,
         verificationStatus,
-        killAllButton
     );
     context.subscriptions.push(verificationManager);
 

diff --git a/src/server.ts b/src/server.ts
@@ -10,6 +10,10 @@ const server = new ServerManager(
     util.log
 );
 
+export function showLogs(): void {
+    serverChannel.show();
+}
+
 server.waitForUnrecoverable().then(() => {
     util.log(`Prusti server is unrecorevable.`);
     address = undefined;
@@ -31,8 +35,8 @@ export function registerCrashHandler(context: vscode.ExtensionContext, verificat
         // Ask the user to restart the server
         util.userErrorPopup(
             "Prusti server stopped working. " +
-            "We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). " +
-            "See the log (View -> Output -> Prusti Assistant Server) for more details.",
+            "If the issue persists, please open a [bug report](https://github.com/viperproject/prusti-dev/issues/new). " +
+            "See [the server logs](command:prusti-assistant.openServerLogs) for more details.",
             "Restart Server",
             () => {
                 restart(context, verificationStatus).then(

diff --git a/src/util.ts b/src/util.ts
@@ -80,6 +80,9 @@ export function log(message: string): void {
     console.log(message);
     logChannel.appendLine(message);
 }
+export function showLogs(): void {
+    logChannel.show();
+}
 
 export type Duration = [seconds: number, nanoseconds: number];
 export type KillFunction = () => void;