From f93022f7e8502e462988f7e1d48ad5b0dfa5ab40 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 8 Aug 2023 12:23:10 +0200 Subject: [PATCH] Show commands in tooltip (closes #223) --- package.json | 2 +- src/diagnostics.ts | 15 +++++++-------- src/extension.ts | 44 ++++++++++++++++++++++++++++---------------- src/server.ts | 8 ++++++-- src/util.ts | 3 +++ 5 files changed, 45 insertions(+), 27 deletions(-) diff --git a/package.json b/package.json index 8db70a0b..d6c8a21f 100644 --- 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 index 9ca7a735..0e34ddb8 100644 --- a/src/diagnostics.ts +++ b/src/diagnostics.ts @@ -562,13 +562,11 @@ export class DiagnosticsManager { private target: vscode.DiagnosticCollection; private procDestructors: Set = 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 index 0901b75e..e9c8b66e 100644 --- a/src/extension.ts +++ b/src/extension.ts @@ -12,7 +12,18 @@ export async function activate(context: vscode.ExtensionContext): Promise 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 ); // 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 const verificationManager = new diagnostics.DiagnosticsManager( verificationDiagnostics, verificationStatus, - killAllButton ); context.subscriptions.push(verificationManager); diff --git a/src/server.ts b/src/server.ts index 8988addf..45f59354 100644 --- 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 index 00278c69..916f8155 100644 --- 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;