Integrate the documentation generator

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",

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<void> {
+        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 {

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))
     }

client/src/ViperProtocol.ts

@@ -64,6 +64,7 @@ export class Commands {
     static FlushCache: RequestType<FlushCacheParams, void, void> = new RequestType("FlushCache");
     //The server requests the identifier at some location in the current file to answer the gotoDefinition request
     static GetIdentifier: RequestType<Position, GetIdentifierResponse, void> = new RequestType("GetIdentifier");
+    static GetDocumentation: RequestType<GetDocumentationRequest, GetDocumentationResponse, void> = 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 }

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);
+    }
+}