Add codelens command to copy models (#18)

Author: wintersteiger

package-lock.json

@@ -6,7 +6,7 @@
   "publisher": "Imandra",
   "icon": "assets/vscode-imandra-avatar.png",
   "license": "MIT",
-  "version": "0.0.10",
+  "version": "0.0.11",
   "repository": {
     "type": "git",
     "url": "https://github.com/imandra-ai/imandrax-vscode"

package.json

@@ -22,6 +22,7 @@ import {
 	Executable,
 	LanguageClient,
 	LanguageClientOptions,
+	VersionedTextDocumentIdentifier,
 } from "vscode-languageclient/node";
 
 const MAX_RESTARTS: number = 10;
@@ -168,6 +169,8 @@ export async function start() {
 
 	client.onRequest("$imandrax/interact-model", (params) => { interact_model(params); });
 
+	client.onRequest("$imandrax/copy-model", (params) => { copy_model(params); });
+
 	// Start the client. This will also launch the server.
 	client.start();
 }
@@ -285,6 +288,16 @@ function interact_model(params) {
 	t.show();
 }
 
+function copy_model(params) {
+	const models = params["models"];
+	let str = "";
+	models.join();
+	models.forEach(async m => {
+		str += m;
+	});
+	env.clipboard.writeText(str);
+}
+
 function clear_cache() {
 	client.sendRequest("workspace/executeCommand", { "command": "clear-cache", "arguments": [] });
 	return true;