From 23251ae25f3d9018d811b73a7b521a5bc3229e17 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 3 Oct 2023 12:45:16 +0200 Subject: [PATCH 1/2] Add a status bar item Add a status bar item to display vscoqtop info (version and coq version). --- client/src/extension.ts | 13 +++++++++- client/src/utilities/toolchain.ts | 41 ++++++++++++++++++++++++++++-- client/src/utilities/versioning.ts | 2 +- 3 files changed, 52 insertions(+), 4 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index 73e4ecf85..5a3d1e93d 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -6,7 +6,9 @@ import {workspace, window, commands, ExtensionContext, TextEditorRevealType, Selection, Uri, - extensions + StatusBarItem, + extensions, + StatusBarAlignment } from 'vscode'; import { @@ -37,6 +39,7 @@ import { } from './utilities/utils'; import { DocumentStateViewProvider } from './panels/DocumentStateViewProvider'; import VsCoqToolchainManager, {ToolchainError, ToolChainErrorCode} from './utilities/toolchain'; +import { stat } from 'fs'; let client: Client; @@ -124,6 +127,10 @@ export function activate(context: ExtensionContext) { const documentStateProvider = new DocumentStateViewProvider(client); context.subscriptions.push(workspace.registerTextDocumentContentProvider("vscoq-document-state", documentStateProvider)); + //status bar item for showing coq version and language server version + const statusBar: StatusBarItem = window.createStatusBarItem(StatusBarAlignment.Right, 1000); + context.subscriptions.push(statusBar); + const launchQuery = (editor: TextEditor, type: string)=> { const selection = editor.selection; const {end, start} = selection; @@ -169,6 +176,10 @@ export function activate(context: ExtensionContext) { .then(() => { checkVersion(client, context); + const serverInfo = client.initializeResult!.serverInfo; + statusBar.text = `${serverInfo?.name} ${serverInfo?.version}, coq ${coqTM.getCoqVersion()}`; + statusBar.tooltip = coqTM.getversionFullOutput(); + statusBar.show(); initializeDecorations(context); diff --git a/client/src/utilities/toolchain.ts b/client/src/utilities/toolchain.ts index 1c85a0487..503d44f90 100644 --- a/client/src/utilities/toolchain.ts +++ b/client/src/utilities/toolchain.ts @@ -6,6 +6,8 @@ import { isFileInFolder } from './fileHelper'; import { ServerSessionOptions } from 'http2'; import { ServerOptions } from 'vscode-languageclient/node'; import Client from '../client'; +import { version } from 'os'; +import { match } from 'assert'; export enum ToolChainErrorCode { notFound = 1, @@ -20,7 +22,9 @@ export interface ToolchainError { export default class VsCoqToolchainManager implements Disposable { - private _vscoqtopPath: string = ""; + private _vscoqtopPath: string = ""; + private _coqVersion: string = ""; + private _versionFullOutput: string = ""; public dispose(): void { @@ -64,6 +68,14 @@ export default class VsCoqToolchainManager implements Disposable { return serverOptions; }; + public getCoqVersion() : string { + return this._coqVersion; + }; + + public getversionFullOutput() : string { + return this._versionFullOutput; + } + private getEnvPath() : string { if(process.platform === 'win32') { return process.env.Path ?? ''; @@ -114,11 +126,36 @@ export default class VsCoqToolchainManager implements Disposable { This could be due to a bad Coq or installation or an incompatible Coq version.` }); } else { - resolve(); + this.coqVersion().then(() => { + resolve(); + }); } }); }); }; + private coqVersion() : Promise { + + const config = workspace.getConfiguration('vscoq').get('args') as string[]; + const options = ["-v"].concat(config); + const cmd = [this._vscoqtopPath].concat(options).join(' '); + + return new Promise((resolve, reject: () => void) => { + exec(cmd, (error, stdout, stderr) => { + if(error) { + reject(); + } else { + const versionRegexp = /\b\d\.\d+(\.\d|\+rc\d)\b/g; + this._versionFullOutput = stdout; + const matchArray = stdout.match(versionRegexp); + if(matchArray) { + this._coqVersion = matchArray[0]; + } + resolve(); + } + }); + }); + }; + } \ No newline at end of file diff --git a/client/src/utilities/versioning.ts b/client/src/utilities/versioning.ts index 9f4cf0a05..5bdfa23db 100644 --- a/client/src/utilities/versioning.ts +++ b/client/src/utilities/versioning.ts @@ -7,7 +7,7 @@ export const checkVersion = (client: Client, context: ExtensionContext) => { const extensionVersion = context.extension.packageJSON.version; const initializeResult = client.initializeResult; if(initializeResult !== undefined) { - const serverInfo =client.initializeResult?.serverInfo; + const serverInfo = client.initializeResult?.serverInfo; if(serverInfo !== undefined) { const {name, version} = serverInfo; Client.writeToVscoq2Channel("[Versioning] Intialized server " + name + " [" + version + "]"); From 6ec0be04fa62f94f2082faac9ee5cb9353362030 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 3 Oct 2023 18:12:21 +0200 Subject: [PATCH 2/2] Finished status bar - Made sure all promises resolve or reject - Added a markdown string on hover --- client/src/extension.ts | 18 ++++++++++++++-- client/src/utilities/toolchain.ts | 34 +++++++++++++++++++++++-------- 2 files changed, 42 insertions(+), 10 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index 5a3d1e93d..da876f357 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -8,7 +8,8 @@ import {workspace, window, commands, ExtensionContext, Uri, StatusBarItem, extensions, - StatusBarAlignment + StatusBarAlignment, + MarkdownString } from 'vscode'; import { @@ -178,7 +179,20 @@ export function activate(context: ExtensionContext) { checkVersion(client, context); const serverInfo = client.initializeResult!.serverInfo; statusBar.text = `${serverInfo?.name} ${serverInfo?.version}, coq ${coqTM.getCoqVersion()}`; - statusBar.tooltip = coqTM.getversionFullOutput(); + statusBar.tooltip = new MarkdownString( + +`**Coq Installation** + +${coqTM.getversionFullOutput()} + +Path: \`${coqTM.getCoqPath()}\` +--- + +**vscoqtop** ${serverInfo?.version} + +Path: \`${coqTM.getVsCoqTopPath()}\` +` + ); statusBar.show(); initializeDecorations(context); diff --git a/client/src/utilities/toolchain.ts b/client/src/utilities/toolchain.ts index 503d44f90..45e7bbe70 100644 --- a/client/src/utilities/toolchain.ts +++ b/client/src/utilities/toolchain.ts @@ -11,8 +11,7 @@ import { match } from 'assert'; export enum ToolChainErrorCode { notFound = 1, - launchError = 2, - coqVersionMissmatch = 3 + launchError = 2 } export interface ToolchainError { @@ -25,6 +24,7 @@ export default class VsCoqToolchainManager implements Disposable { private _vscoqtopPath: string = ""; private _coqVersion: string = ""; private _versionFullOutput: string = ""; + private _coqPath: string = ""; public dispose(): void { @@ -68,6 +68,14 @@ export default class VsCoqToolchainManager implements Disposable { return serverOptions; }; + public getVsCoqTopPath() : string { + return this._vscoqtopPath; + } + + public getCoqPath() : string { + return this._coqPath; + } + public getCoqVersion() : string { return this._coqVersion; }; @@ -123,12 +131,22 @@ export default class VsCoqToolchainManager implements Disposable { reject({ status: ToolChainErrorCode.launchError, message: `${this._vscoqtopPath} crashed with the following message: ${stderr} - This could be due to a bad Coq or installation or an incompatible Coq version.` + This could be due to a bad Coq installation or an incompatible Coq version.` }); } else { - this.coqVersion().then(() => { - resolve(); - }); + this._coqPath = stdout; + this.coqVersion().then( + () => { + resolve(); + }, + (err) => { + reject({ + status: ToolChainErrorCode.launchError, + message: `${this._vscoqtopPath} crashed with the following message: ${err}. + This could be due to a bad Coq installation or an incompatible Coq version` + }); + } + ); } }); @@ -141,10 +159,10 @@ export default class VsCoqToolchainManager implements Disposable { const options = ["-v"].concat(config); const cmd = [this._vscoqtopPath].concat(options).join(' '); - return new Promise((resolve, reject: () => void) => { + return new Promise((resolve, reject: (reason: string) => void) => { exec(cmd, (error, stdout, stderr) => { if(error) { - reject(); + reject(stderr); } else { const versionRegexp = /\b\d\.\d+(\.\d|\+rc\d)\b/g; this._versionFullOutput = stdout;