Add custom editors for krml and checked files.

FStarLang · Oct 11, 2024 · 7e7ed9b · 7e7ed9b
1 parent 94a42f9
commit 7e7ed9b
Show file tree

Hide file tree

Showing 5 changed files with 95 additions and 0 deletions.
diff --git a/client/package-lock.json b/client/package-lock.json
diff --git a/client/package.json b/client/package.json
@@ -16,6 +16,7 @@
 		"compile": "esbuild --bundle src/extension.ts --outfile=out/extension.js --tsconfig=tsconfig.json --platform=node --external:vscode --sourcemap --preserve-symlinks --sources-content=false"
 	},
 	"dependencies": {
+		"html-escaper": "^3.0.3",
 		"vscode-languageclient": "^9.0.1"
 	},
 	"devDependencies": {

diff --git a/client/src/binaryeditors.ts b/client/src/binaryeditors.ts
@@ -0,0 +1,55 @@
+/* --------------------------------------------------------------------------------------------
+ * Copyright (c) Microsoft Corporation. All rights reserved.
+ * Licensed under the MIT License. See License.txt in the project root for license information.
+ * ------------------------------------------------------------------------------------------ */
+
+import { CancellationToken, Command, CustomDocument, CustomDocumentOpenContext, CustomReadonlyEditorProvider, Uri, WebviewPanel } from 'vscode';
+import * as cp from 'child_process';
+import * as util from 'util';
+import { escape } from 'html-escaper';
+
+class CommandOutputDocument implements CustomDocument {
+	constructor(public uri: Uri, public cmd: string, public stdout: string, public stderr: string) {}
+	toHtml(): string {
+		return `<html>
+<head>
+	<style>
+	body {
+		background: var(--vscode-editor-background);
+		color: var(--vscode-editor-foreground);
+	}
+	pre, .code {
+		font-family: var(--vscode-editor-font-family);
+		font-size: var(--vscode-editor-font-size);
+	}
+	</style>
+</head>
+<body>
+<p>Output of <span class="code">${escape(this.cmd)}</span>:</p>
+<pre>
+${escape(this.stdout)}
+<div style="color: var(--vscode-errorForeground)">${escape(this.stderr)}</div>
+</pre>
+`;
+	}
+	dispose(): void {}
+}
+
+abstract class CommandOutputProvider implements CustomReadonlyEditorProvider<CommandOutputDocument> {
+	async openCustomDocument(uri: Uri): Promise<CommandOutputDocument> {
+		const cmd = this.getCommand(uri);
+		const out = await util.promisify(cp.execFile)(cmd[0], cmd.slice(1));
+		return new CommandOutputDocument(uri, cmd.join(' '), out.stdout, out.stderr);
+	}
+	resolveCustomEditor(document: CommandOutputDocument, webviewPanel: WebviewPanel) {
+		webviewPanel.webview.html = document.toHtml();
+	}
+	abstract getCommand(uri: Uri): string[];
+}
+
+export class CheckedFileEditorProvider extends CommandOutputProvider {
+	getCommand(uri: Uri): string[] { return ['fstar.exe', '--read_checked_file', uri.fsPath]; }
+}
+export class KrmlFileEditorProvider extends CommandOutputProvider {
+	getCommand(uri: Uri): string[] { return ['fstar.exe', '--read_krml_file', uri.fsPath]; }
+}
diff --git a/client/src/extension.ts b/client/src/extension.ts
@@ -15,6 +15,7 @@ import {
 	Position
 } from 'vscode-languageclient/node';
 import { StatusNotificationParams, killAllNotification, killAndRestartSolverNotification, restartNotification, statusNotification, verifyToPositionNotification } from './fstarLspExtensions';
+import { CheckedFileEditorProvider, KrmlFileEditorProvider } from './binaryeditors';
 
 let client: LanguageClient;
 
@@ -201,6 +202,9 @@ export async function activate(context: ExtensionContext) {
 		};
 	});
 
+	context.subscriptions.push(vscode.window.registerCustomEditorProvider('fstar.checked', new CheckedFileEditorProvider()));
+	context.subscriptions.push(vscode.window.registerCustomEditorProvider('fstar.krml', new KrmlFileEditorProvider()));
+
 	await client.start();
 }
 

diff --git a/package.json b/package.json
@@ -40,6 +40,29 @@
 				"path": "./syntaxes/fstar.tmLanguage.json"
 			}
 		],
+		"customEditors": [
+			{
+				"viewType": "fstar.checked",
+				"displayName": "F* Checked File",
+				"selector": [
+					{
+						"filenamePattern": "*.fst.checked"
+					},
+					{
+						"filenamePattern": "*.fsti.checked"
+					}
+				]
+			},
+			{
+				"viewType": "fstar.krml",
+				"displayName": "F* Krml File",
+				"selector": [
+					{
+						"filenamePattern": "*.krml"
+					}
+				]
+			}
+		],
 		"configuration": {
 			"type": "object",
 			"title": "F* VSCode Assistant",