diff --git a/client/package-lock.json b/client/package-lock.json index 027d88c1..29878b13 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -32,6 +32,7 @@ "ts-node": "^10.9.2", "typescript": "^5.4.5", "unused-filename": "^3.0.1", + "viperdoc": "git+https://github.com/fnussbaum/viperdoc.git", "vs-verification-toolbox": "git+https://github.com/viperproject/vs-verification-toolbox.git", "vscode-languageclient": "^9.0.1", "vscode-uri": "^3.0.8", @@ -2554,6 +2555,21 @@ "safe-buffer": "^5.0.1" } }, + "node_modules/ejs": { + "version": "3.1.10", + "resolved": "https://registry.npmjs.org/ejs/-/ejs-3.1.10.tgz", + "integrity": "sha512-UeJmFfOrAQS8OJWPZ4qtgHyWExa088/MtK5UEyoJGFH67cDEXkZSviOiKRCZ4Xij0zxI3JECgYs3oKx+AizQBA==", + "dev": true, + "dependencies": { + "jake": "^10.8.5" + }, + "bin": { + "ejs": "bin/cli.js" + }, + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/electron-to-chromium": { "version": "1.4.717", "dev": true, @@ -3124,6 +3140,27 @@ "node": "^10.12.0 || >=12.0.0" } }, + "node_modules/filelist": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/filelist/-/filelist-1.0.4.tgz", + "integrity": "sha512-w1cEuf3S+DrLCQL7ET6kz+gmlJdbq9J7yXCSjK/OZCPA+qEN1WyF4ZAf0YYJa4/shHJra2t/d/r8SV4Ji+x+8Q==", + "dev": true, + "dependencies": { + "minimatch": "^5.0.1" + } + }, + "node_modules/filelist/node_modules/minimatch": { + "version": "5.1.6", + "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.6.tgz", + "integrity": "sha512-lKwV/1brpG6mBUFHtb7NUmtABCb2WZZmm2wNiOA5hAb8VdCS4B3dtMWyvcoViccwAW/COERjXLt0zP1zXUN26g==", + "dev": true, + "dependencies": { + "brace-expansion": "^2.0.1" + }, + "engines": { + "node": ">=10" + } + }, "node_modules/fill-range": { "version": "7.0.1", "dev": true, @@ -3580,6 +3617,15 @@ "he": "bin/he" } }, + "node_modules/highlight.js": { + "version": "11.10.0", + "resolved": "https://registry.npmjs.org/highlight.js/-/highlight.js-11.10.0.tgz", + "integrity": "sha512-SYVnVFswQER+zu1laSya563s+F8VDGt7o35d4utbamowvUNLLMovFqwCLSocpZTz3MgaSRA1IbqRWZv97dtErQ==", + "dev": true, + "engines": { + "node": ">=12.0.0" + } + }, "node_modules/hosted-git-info": { "version": "4.1.0", "dev": true, @@ -4116,6 +4162,116 @@ "@pkgjs/parseargs": "^0.11.0" } }, + "node_modules/jake": { + "version": "10.9.2", + "resolved": "https://registry.npmjs.org/jake/-/jake-10.9.2.tgz", + "integrity": "sha512-2P4SQ0HrLQ+fw6llpLnOaGAvN2Zu6778SJMrCUwns4fOoG9ayrTiZk3VV8sCPkVZF8ab0zksVpS8FDY5pRCNBA==", + "dev": true, + "dependencies": { + "async": "^3.2.3", + "chalk": "^4.0.2", + "filelist": "^1.0.4", + "minimatch": "^3.1.2" + }, + "bin": { + "jake": "bin/cli.js" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/jake/node_modules/ansi-styles": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", + "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, + "dependencies": { + "color-convert": "^2.0.1" + }, + "engines": { + "node": ">=8" + }, + "funding": { + "url": "https://github.com/chalk/ansi-styles?sponsor=1" + } + }, + "node_modules/jake/node_modules/brace-expansion": { + "version": "1.1.11", + "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz", + "integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==", + "dev": true, + "dependencies": { + "balanced-match": "^1.0.0", + "concat-map": "0.0.1" + } + }, + "node_modules/jake/node_modules/chalk": { + "version": "4.1.2", + "resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz", + "integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==", + "dev": true, + "dependencies": { + "ansi-styles": "^4.1.0", + "supports-color": "^7.1.0" + }, + "engines": { + "node": ">=10" + }, + "funding": { + "url": "https://github.com/chalk/chalk?sponsor=1" + } + }, + "node_modules/jake/node_modules/color-convert": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", + "integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==", + "dev": true, + "dependencies": { + "color-name": "~1.1.4" + }, + "engines": { + "node": ">=7.0.0" + } + }, + "node_modules/jake/node_modules/color-name": { + "version": "1.1.4", + "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz", + "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==", + "dev": true + }, + "node_modules/jake/node_modules/has-flag": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz", + "integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==", + "dev": true, + "engines": { + "node": ">=8" + } + }, + "node_modules/jake/node_modules/minimatch": { + "version": "3.1.2", + "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.1.2.tgz", + "integrity": "sha512-J7p63hRiAjw1NDEww1W7i37+ByIrOWO5XQQAzZ3VOcL0PNybwpfmV/N05zFAzwQ9USyEcX6t3UO+K5aqBQOIHw==", + "dev": true, + "dependencies": { + "brace-expansion": "^1.1.7" + }, + "engines": { + "node": "*" + } + }, + "node_modules/jake/node_modules/supports-color": { + "version": "7.2.0", + "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz", + "integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==", + "dev": true, + "dependencies": { + "has-flag": "^4.0.0" + }, + "engines": { + "node": ">=8" + } + }, "node_modules/jest-util": { "version": "29.7.0", "dev": true, @@ -4631,6 +4787,18 @@ "url": "https://github.com/fb55/entities?sponsor=1" } }, + "node_modules/marked": { + "version": "12.0.2", + "resolved": "https://registry.npmjs.org/marked/-/marked-12.0.2.tgz", + "integrity": "sha512-qXUm7e/YKFoqFPYPa3Ukg9xlI5cyAtGmyEIzMfW//m6kXwCy2Ps9DYf5ioijFKQ8qyuscrHoY04iJGctu2Kg0Q==", + "dev": true, + "bin": { + "marked": "bin/marked.js" + }, + "engines": { + "node": ">= 18" + } + }, "node_modules/mdurl": { "version": "1.0.1", "dev": true, @@ -4975,8 +5143,9 @@ }, "node_modules/npm-run-all": { "version": "4.1.5", + "resolved": "https://registry.npmjs.org/npm-run-all/-/npm-run-all-4.1.5.tgz", + "integrity": "sha512-Oo82gJDAVcaMdi3nuoKFavkIHBRVqQ1qvMb+9LHk/cF4P6B2m8aP04hGf7oL6wZ9BuGwX1onlLhpuoofSyoQDQ==", "dev": true, - "license": "MIT", "dependencies": { "ansi-styles": "^3.2.1", "chalk": "^2.4.1", @@ -6933,6 +7102,18 @@ "spdx-expression-parse": "^3.0.0" } }, + "node_modules/viperdoc": { + "version": "1.0.0", + "resolved": "git+ssh://git@github.com/fnussbaum/viperdoc.git#8cd5c276fad992b99c072444ad835c14cc9d9a9a", + "dev": true, + "license": "ISC", + "dependencies": { + "ejs": "^3.1.10", + "fs-extra": "^11.2.0", + "highlight.js": "^11.9.0", + "marked": "^12.0.2" + } + }, "node_modules/vs-verification-toolbox": { "version": "1.0.0", "resolved": "git+ssh://git@github.com/viperproject/vs-verification-toolbox.git#c90fd1c4871dfc0e1616621c824af9a59b94a78d", diff --git a/client/package.json b/client/package.json index ed8e7953..a7196944 100644 --- a/client/package.json +++ b/client/package.json @@ -57,6 +57,7 @@ "ts-node": "^10.9.2", "typescript": "^5.4.5", "unused-filename": "^3.0.1", + "viperdoc": "git+https://github.com/fnussbaum/viperdoc.git", "vs-verification-toolbox": "git+https://github.com/viperproject/vs-verification-toolbox.git", "vscode-languageclient": "^9.0.1", "vscode-uri": "^3.0.8", @@ -131,6 +132,11 @@ "title": "flush the cache for this file", "category": "Viper" }, + { + "command": "viper.viperdocGenerate", + "title": "generate documentation website for this file", + "category": "Viper" + }, { "command": "viper.showSettings", "title": "display settings effectively used by Viper-IDE", diff --git a/client/src/ExtensionState.ts b/client/src/ExtensionState.ts index 74bf72f8..0a6ea8e7 100644 --- a/client/src/ExtensionState.ts +++ b/client/src/ExtensionState.ts @@ -14,8 +14,9 @@ import * as path from 'path'; import * as readline from 'readline'; import * as semver from 'semver'; import unusedFilename from 'unused-filename'; +import { generateWebsite } from 'viperdoc'; import { Location } from 'vs-verification-toolbox'; -import { Backend, Commands, Common, GetVersionRequest, LogLevel } from './ViperProtocol'; +import { Backend, Commands, Common, GetVersionRequest, LogLevel, GetDocumentationRequest } from './ViperProtocol'; import { Log } from './Log'; import { ViperFileState } from './ViperFileState'; import { URI } from 'vscode-uri'; @@ -28,7 +29,7 @@ import { combineMessages, Either, Messages, newEitherError, newRight, transformR export class State { public static get MIN_SERVER_VERSION(): string { - return "2.0.0"; // has to be a valid semver + return "2.0.0"; // has to be a valid server } public static client: LanguageClient; @@ -204,7 +205,7 @@ export class State { synchronize: { // Synchronize the setting section 'viperSettings' to the server configurationSection: 'viperSettings', - // Notify the server about file changes to .sil or .vpr files contain in the workspace + // Notify the server about file changes to .sil or .vpr files contained in the workspace fileEvents: fileSystemWatcher }, // redirect output while unit testing to the log file as no UI is available, otherwise stick to default behavior, i.e. separate output view @@ -337,6 +338,12 @@ export class State { } State.reset(); } + + public static async getDocumentation(uri: vscode.Uri): Promise { + const params: GetDocumentationRequest = { uri: uri.toString() }; + const response = await State.client.sendRequest(Commands.GetDocumentation, params); + await generateWebsite(uri.fsPath, response.documentation, path.join(this.context.extensionPath, "node_modules", "viperdoc")); + } } export interface UnitTestCallback { diff --git a/client/src/ViperApi.ts b/client/src/ViperApi.ts index 0c53e8d5..3408f574 100644 --- a/client/src/ViperApi.ts +++ b/client/src/ViperApi.ts @@ -42,7 +42,7 @@ export class ViperApi { this.verificationTerminatedObservers.push(callback); } - /** Notify a VerificationTermianted event to all observers. */ + /** Notify a VerificationTerminated event to all observers. */ public notifyVerificationTerminated(event: VerificationTerminatedEvent): void { this.verificationTerminatedObservers.forEach(callback => callback(event)) } diff --git a/client/src/ViperProtocol.ts b/client/src/ViperProtocol.ts index 61848cd6..d8e6cfc2 100644 --- a/client/src/ViperProtocol.ts +++ b/client/src/ViperProtocol.ts @@ -64,6 +64,7 @@ export class Commands { static FlushCache: RequestType = new RequestType("FlushCache"); //The server requests the identifier at some location in the current file to answer the gotoDefinition request static GetIdentifier: RequestType = new RequestType("GetIdentifier"); + static GetDocumentation: RequestType = new RequestType("GetDocumentation"); } //============================================================================== @@ -341,6 +342,14 @@ export interface GetIdentifierResponse { identifier: string // nullable } +export interface GetDocumentationRequest { + uri: string, +} + +export interface GetDocumentationResponse { + documentation: string // nullable +} + //Communication between Language Server and Debugger: export enum StepType { Stay, Next, Back, In, Out, Continue } diff --git a/client/src/extension.ts b/client/src/extension.ts index bb6d578f..e760d12a 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -320,6 +320,11 @@ function registerContextHandlers(context: vscode.ExtensionContext, location: Loc //remove diagnostics of open file context.subscriptions.push(vscode.commands.registerCommand('viper.removeDiagnostics', () => removeDiagnostics(true))); + // Viperdoc: generate documentation website + context.subscriptions.push(vscode.commands.registerCommand('viper.viperdocGenerate', () => { + viperdocGenerate(); + })); + // show currently active (Viper) settings context.subscriptions.push(vscode.commands.registerCommand('viper.showSettings', async () => { const settings = vscode.workspace.getConfiguration("viperSettings"); @@ -462,3 +467,10 @@ function removeDiagnostics(activeFileOnly: boolean): void { Log.log(`All diagnostics successfully removed`, LogLevel.Debug); } } + +function viperdocGenerate(): void { + if (vscode.window.activeTextEditor) { + const uri = vscode.window.activeTextEditor.document.uri; + void State.getDocumentation(uri); + } +}