Add command to open VFS files

Author: wintersteiger

.gitignore

@@ -2,3 +2,4 @@ out
 node_modules
 .vscode-test
 *.vsix
+tmp

.vscodeignore

@@ -16,4 +16,6 @@ src/node_modules/**
 !src/node_modules/vscode-languageserver-protocol/**
 !src/node_modules/vscode-languageserver-types/**
 !src/node_modules/{minimatch,brace-expansion,concat-map,balanced-match}/**
-!src/node_modules/{semver,lru-cache,yallist}/**
+!src/node_modules/{semver,lru-cache,yallist}/**
+tmp
+_opam

package.json

@@ -5,7 +5,7 @@
   "author": "Imandra Inc",
   "publisher": "imandra",
   "license": "MIT",
-  "version": "0.0.6",
+  "version": "0.0.7",
   "repository": {
     "type": "git",
     "url": "https://github.com/imandra-ai/imandrax-vscode"
@@ -132,6 +132,10 @@
       {
         "command": "imandrax.clear_cache",
         "title": "ImandraX: Clear cache"
+      },
+      {
+        "command": "imandrax.open_vfs_file",
+        "title": "Imandrax: open VFS file"
       }
     ]
   },

src/extension.ts

@@ -8,7 +8,8 @@ import {
 	env,
 	Uri,
 	TerminalOptions,
-	Range
+	Range,
+	TextDocumentContentProvider
 } from "vscode";
 
 import {
@@ -59,6 +60,24 @@ export function activate(context: ExtensionContext) {
 	const clear_cache_handler = () => { clear_cache(); };
 	context.subscriptions.push(commands.registerCommand(clear_cache_cmd, clear_cache_handler));
 
+	const open_vfs_file_cmd = "imandrax.open_vfs_file";
+	const open_vfs_file_handler = async () => {
+		const what = await window.showInputBox({ placeHolder: 'file name?' });
+		if (what) {
+			const uri = Uri.parse(what);
+			const doc = await workspace.openTextDocument(uri);
+			await window.showTextDocument(doc, { preview: false });
+		}
+	};
+	context.subscriptions.push(commands.registerCommand(open_vfs_file_cmd, open_vfs_file_handler));
+
+	const vfs_provider = new (class implements TextDocumentContentProvider {
+		async provideTextDocumentContent(uri: Uri): Promise<string> {
+			return await client.sendRequest<string>("$imandrax/req-vfs-file", { "uri": uri } );
+		}
+	})();
+	context.subscriptions.push(workspace.registerTextDocumentContentProvider("imandrax-vfs", vfs_provider));
+
 	// Start language server
 	const config = workspace.getConfiguration("imandrax");
 	const binary = config.lsp.binary;