Version 0.2.0

.vscode/settings.json

@@ -12,6 +12,10 @@
     "**/CVS": true,
     "**/.DS_Store": true,
     "**/Thumbs.db": true,
+    "**/.*.aux": true,
+    "**/.lia.cache": true,
+    "**/.nia.cache": true,
+    "**/.nra.cache": true,
     "**/.classpath": true,
     "**/.project": true,
     "**/.settings": true,

package.json

@@ -1,8 +1,8 @@
 {
   "name": "vizx",
-  "displayName": "ViZX",
+  "displayName": "ZXViz",
   "description": "Visualizer for the ZX calculus",
-  "version": "0.1.4",
+  "version": "0.2.0",
   "repository": "https://github.com/inQWIRE/ViZX/",
   "publisher": "inQWIRE",
   "engines": {
@@ -12,11 +12,13 @@
     "Other"
   ],
   "activationEvents": [
-    "onCommand:vizx.render",
-    "onCommand:vizx.lspRender",
-    "onCommand:vizx.activateRendering"
+    "onLanguage:coq",
+    "onLanguage:rocq"
   ],
   "main": "./out/extension.js",
+  "extensionDependencies": [
+    "ejgallego.coq-lsp"
+  ],
   "contributes": {
     "commands": [
       {
@@ -35,21 +37,39 @@
         "command": "vizx.deactivateRendering",
         "title": "ZXViz: Deactivate ZXViz automatic rendering"
       }
-    ]
+    ],
+    "configuration": {
+      "type": "object",
+      "title": "ViZX Extension Configuration",
+      "properties": {
+        "vizx.ignoreActiveVsCoq": {
+          "type": "boolean",
+          "default": false,
+          "description": "Allow ViZX to run with VSCoq active despite possible issues. Setting to true will disable bug reporting features, as this is not officially supported."
+        },
+        "vizx.enableAutomaticRendering": {
+          "type": "boolean",
+          "default": true,
+          "description": "Enable automatic rendering of ZX diagrams when the file is saved or the editor is focused. Disable this to manually trigger rendering."
+        }
+      }
+    }
   },
   "scripts": {
     "vscode:prepublish": "npm run package",
     "compile": "node ./esbuild.js",
     "package": "NODE_ENV=production node ./esbuild.js",
-    "watch": "node ./esbuild.js --watch",
+    "watch": "node ./esbuild.js & node ./esbuild.js --watch",
     "lint": "eslint src --ext ts & npx prettier --write .",
-    "deploy": "vsce publish"
+    "deploy": "vsce publish",
+    "check-types": "tsc --noEmit"
   },
   "devDependencies": {
     "@babel/core": "^7.21.4",
     "@babel/preset-env": "^7.21.4",
     "@babel/preset-typescript": "^7.21.4",
     "@types/glob": "^7.2.0",
+    "@types/minimatch": "^6.0.0",
     "@types/node": "14.x",
     "@types/vscode": "^1.74.0",
     "@typescript-eslint/eslint-plugin": "^5.16.0",
@@ -61,7 +81,8 @@
     "glob": "^7.2.0",
     "lodash": "^4.17.21",
     "prettier": "2.8.4",
-    "typescript": "^4.5.5"
+    "typescript": "^4.5.5",
+    "vscode-languageserver-types": "^3.17.5"
   },
   "dependencies": {
     "deep-object-diff": "^1.1.9",

src/constants/consts.ts

@@ -11,6 +11,7 @@ export const STACK_OP = "↕"; // \updownarrow
 export const N_STACK_1_OP = "↑";
 
 export const PROP_TO = "∝";
+export const EQ = "=";
 export const CAP = "⊂";
 export const CUP = "⊃";
 export const WIRE = "—";

src/extension.ts

@@ -1,21 +1,16 @@
 // The module 'vscode' contains the VS Code extensibility API
 // Import the module and reference it with the alias vscode in your code below
 import * as vscode from "vscode";
-import * as parser from "./parsing/parser";
-import * as sizer from "./parsing/sizes";
-import * as coord from "./parsing/coords";
-import { boundary, setCanvasWidthHeight } from "./constants/variableconsts";
-import * as vconsts from "./constants/variableconsts";
-import * as ast from "./parsing/ast";
-import { getCanvasHtml } from "./webview/webview";
+import { coqLspApi, only_with_lsp } from "./lspguards";
+import { render, renderCallback } from "./rendering/callback";
 
-let openWebview: vscode.WebviewPanel | undefined = undefined;
 let history: string[] = [];
 const HISTORY_LENGTH = vscode.workspace
   .getConfiguration("vizx")
   .get<number>("historyLength", 25);
 const HISTORY_KEY = "vizxInputHistory";
 
+let hook: vscode.Disposable | undefined = undefined;
 // this method is called when your extension is activated
 // your extension is activated the very first time the command is executed
 export function activate(context: vscode.ExtensionContext) {
@@ -26,121 +21,168 @@ export function activate(context: vscode.ExtensionContext) {
   // The command has been defined in the package.json file
   // Now provide the implementation of the command with registerCommand
   // The commandId parameter must match the command field in package.json
-  let disposable = vscode.commands.registerCommand("vizx.render", () => {
-    const newDiag = "New...";
-    const inputBox = vscode.window
-      .showQuickPick([...history, newDiag], {
-        placeHolder: "Diagram syntax with notations",
-        title: "Enter or choose diagram",
-      })
-      .then((selected) => {
-        if (selected === undefined) {
-          return;
-        } else if (selected === newDiag) {
-          vscode.window
-            .showInputBox({ prompt: "Enter diagram syntax with notations" })
-            .then((value) => {
-              if (value) {
-                history.unshift(value); // Add to history
-                if (history.length > HISTORY_LENGTH) {
-                  history.pop(); // Limit history size
-                }
-                context.workspaceState.update(HISTORY_KEY, history); // Save to workspaceState
-                renderCallback(context, value);
-              }
-            });
-        } else {
-          history = history.filter((item) => item !== selected);
-          history.unshift(selected); // Add to the front of history
-          context.workspaceState.update(HISTORY_KEY, history);
-          renderCallback(context, selected);
-        }
-      });
-  });
+  let disposables = [
+    vscode.commands.registerCommand("vizx.render", () =>
+      renderCommand(context)
+    ),
+  ];
+
+  disposables.push(
+    vscode.commands.registerCommand("vizx.lspRender", (expr) =>
+      renderCallback(context, expr)
+    )
+  );
 
-  context.subscriptions.push(disposable);
-  disposable = vscode.commands.registerCommand("vizx.lspRender", (expr) =>
-    renderCallback(context, expr)
+  disposables.push(
+    vscode.commands.registerCommand("vizx.activateRendering", () =>
+      activateRenderingCommand(context)
+    )
   );
-  context.subscriptions.push(disposable);
-  let coqLspApi = vscode.extensions.getExtension("ejgallego.coq-lsp")!.exports;
-  let hook = coqLspApi.onUserGoals((goals: any) =>
-    vscode.commands.executeCommand("vizx.lspRender", goals)
+  disposables.push(
+    vscode.commands.registerCommand("vizx.deactivateRendering", () =>
+      deactivateRenderingCommand()
+    )
   );
+  context.subscriptions.push(...disposables);
 
-  disposable = vscode.commands.registerCommand("vizx.activateRendering", () => {
-    vscode.window.showInformationMessage(
-      "Automatic rendering is now turned on."
-    );
-  });
-  context.subscriptions.push(disposable);
-  disposable = vscode.commands.registerCommand(
-    "vizx.deactivateRendering",
-    () => {
-      deactivate();
-      vscode.window.showInformationMessage(
-        "Automatic rendering is now turned off."
+  const config = vscode.workspace.getConfiguration("vizx");
+  const autoRenderingEnabled = config.get<boolean>(
+    "enableAutomaticRendering",
+    false
+  );
+  if (autoRenderingEnabled) {
+    // Wait until a tab named "goals" exists before activating rendering
+    activateRendering(context);
+    if (hook === undefined) {
+      vscode.window.showWarningMessage(
+        "Automatic rendering is enabled, but the LSP hook could not be set up. Please ensure that the Coq LSP is running."
       );
-      hook.dispose();
     }
-  );
+    vscode.window.showInformationMessage(
+      "ViZX automatic rendering is now turned on."
+    );
+  } else {
+    vscode.window
+      .showInformationMessage(
+        "ViZX automatic rendering is currently disabled.",
+        "Enable",
+        "OK"
+      )
+      .then((selection) => {
+        if (selection === "Enable") {
+          vscode.commands.executeCommand("vizx.activateRendering");
+        }
+      });
+  }
+}
 
-  context.subscriptions.push(disposable);
+function renderCommand(context: vscode.ExtensionContext): void {
+  const newDiag = "New...";
+  vscode.window
+    .showQuickPick([...history, newDiag], {
+      placeHolder: "Diagram syntax with notations",
+      title: "Enter or choose diagram",
+    })
+    .then((selected) => {
+      if (selected === undefined) {
+        return;
+      } else if (selected === newDiag) {
+        vscode.window
+          .showInputBox({ prompt: "Enter diagram syntax with notations" })
+          .then((value) => {
+            if (value) {
+              history.unshift(value); // Add to history
+              if (history.length > HISTORY_LENGTH) {
+                history.pop(); // Limit history size
+              }
+              context.workspaceState.update(HISTORY_KEY, history); // Save to workspaceState
+              render(context, value);
+            }
+          });
+      } else {
+        history = history.filter((item) => item !== selected);
+        history.unshift(selected); // Add to the front of history
+        context.workspaceState.update(HISTORY_KEY, history);
+        render(context, selected);
+      }
+    });
 }
 
-function renderCallback(context: vscode.ExtensionContext, expr: any) {
-  {
-    if (expr === undefined) {
-      console.log("no expression to be rendered");
-      return;
-    }
-    if (expr.goals !== undefined) {
-      // extract correct field from lsp information
-      expr = expr.goals.goals[0].ty.toString();
-    }
-    console.log("expr: ", expr);
-    let node: ast.ASTNode;
-    try {
-      node = parser.parseAST(expr);
-      node = sizer.addSizes(node);
-      console.log("sized node: ", node);
-      const size = sizer.determineCanvasWidthHeight(node);
-      setCanvasWidthHeight(size);
-      node = coord.addCoords(node, boundary);
-    } catch (e) {
-      vscode.window.showErrorMessage(
-        `Error rendering your expression (${expr}): ${e}`
-      );
-      return;
-    }
-    if (openWebview !== undefined) {
-      openWebview.dispose();
-    }
-    const panel = vscode.window.createWebviewPanel(
-      "ViZX",
-      `ViZX: ${expr}`,
-      {
-        viewColumn: vscode.ViewColumn.Three,
-        preserveFocus: true,
-      },
-      {
-        enableScripts: true,
-        retainContextWhenHidden: true,
+function activateRenderingCommand(context: vscode.ExtensionContext): void {
+  const config = vscode.workspace.getConfiguration("vizx");
+  const enabled = config.get<boolean>("enableAutomaticRendering", false);
+  if (!enabled) {
+    // if disabled, then ask user if they want to enable it
+    vscode.window
+      .showInformationMessage(
+        "Automatic rendering is currently disabled. Do you want to enable it?",
+        "Enable for this project",
+        "Enable globally"
+      )
+      .then((selection) => {
+        if (selection === "Enable for this project") {
+          config.update(
+            "enableAutomaticRendering",
+            true,
+            vscode.ConfigurationTarget.Workspace
+          );
+        } else if (selection === "Enable globally") {
+          config.update(
+            "enableAutomaticRendering",
+            true,
+            vscode.ConfigurationTarget.Global
+          );
+        }
+        activateRendering(context);
+      });
+    return;
+  }
+  vscode.window.showInformationMessage("Automatic rendering is now turned on.");
+}
+
+function deactivateRenderingCommand(): void {
+  vscode.window
+    .showInformationMessage(
+      "Automatic rendering is now turned off.",
+      "Deactivate for this project",
+      "Deactivate globally"
+    )
+    .then((selection) => {
+      if (selection === "Deactivate for this project") {
+        vscode.workspace
+          .getConfiguration("vizx")
+          .update(
+            "enableAutomaticRendering",
+            false,
+            vscode.ConfigurationTarget.Workspace
+          );
+      } else if (selection === "Deactivate globally") {
+        vscode.workspace
+          .getConfiguration("vizx")
+          .update(
+            "enableAutomaticRendering",
+            false,
+            vscode.ConfigurationTarget.Global
+          );
       }
-    );
-    panel.onDidDispose(
-      async () => {
-        console.log("openWebview before: ", openWebview);
-        openWebview = undefined;
-      },
-      null,
-      context.subscriptions
-    );
-    openWebview = panel;
-    panel.webview.html = getCanvasHtml(panel, context);
-    panel.webview.onDidReceiveMessage((msg) => console.log(msg));
-    panel.webview.postMessage({ command: JSON.stringify(node) });
+    });
+  deactivateRendering();
+}
+
+function activateRendering(context: vscode.ExtensionContext): void {
+  if (hook !== undefined) {
+    return; // no need to recreate as it would be the exact same
   }
+  only_with_lsp(() => {
+    hook = coqLspApi!.onUserGoals((goals: any) =>
+      renderCallback(context, goals)
+    );
+  });
+}
+
+function deactivateRendering() {
+  hook?.dispose();
+  hook = undefined;
 }
 
 // this method is called when your extension is deactivated