Add Zoom & Move Controls to Diagram

client/src/webview/diagram.ts

@@ -0,0 +1,211 @@
+import type { StateMachine } from "../types/fsm";
+
+// constants
+const MIN_ZOOM = 0.2;
+const MAX_ZOOM = 5;
+const ZOOM_BUTTON_FACTOR = 1.2;
+const SCROLL_ZOOM_IN_FACTOR = 1.05;
+const SCROLL_ZOOM_OUT_FACTOR = 0.95;
+
+// state variables
+let zoomLevel = 1;
+let panX = 0;
+let panY = 0;
+let isPanning = false;
+let startX = 0;
+let startY = 0;
+
+/**
+ * Converts a StateMachine object to a Mermaid state diagram string
+ * @param sm 
+ * @returns Mermaid diagram string
+ */
+export function createMermaidDiagram(sm: StateMachine, orientation: "LR" | "TB"): string {
+    if (!sm) return '';
+
+    const lines: string[] = [];
+
+    // header
+    lines.push('---');
+    lines.push(`title: ${sm.className}`);
+    lines.push('---');
+    lines.push('stateDiagram-v2');
+    lines.push(`    direction ${orientation}`);
+
+    // initial states
+    sm.initialStates.forEach(state => {
+        lines.push(`    [*] --> ${state}`);
+    });
+
+    // group transitions by from/to states and merge labels
+    const transitionMap = new Map<string, string[]>();
+    sm.transitions.forEach(transition => {
+        const key = `${transition.from}|${transition.to}`;
+        if (!transitionMap.has(key)) transitionMap.set(key, []);
+        transitionMap.get(key).push(transition.label);
+    });
+
+    // add transitions
+    transitionMap.forEach((labels, key) => {
+        const [from, to] = key.split('|');
+        const mergedLabel = labels.join(', ');
+        lines.push(`    ${from} --> ${to} : ${mergedLabel}`);
+    });
+
+    return lines.join('\n');
+}
+
+/**
+ * Renders Mermaid diagrams in the document
+ * @param document The document object
+ * @param window The window object
+ */
+export async function renderMermaidDiagram(document: any, window: any) {
+    const mermaid = (window as any).mermaid;
+    if (!mermaid) return;
+
+    const mermaidElements = document.querySelectorAll('.mermaid');
+    if (mermaidElements.length === 0) return;
+
+    try { 
+        await mermaid.run({ nodes: mermaidElements });
+        applyTransform(document);
+        registerPanListeners(document);
+    } catch (e) {
+        console.error('Failed to render Mermaid diagram:', e);
+    }
+}
+
+/**
+ * Resets zoom and pan to default values
+ * @param document The document object
+ */
+export function zoomIn(document: any) {
+    const container = document.querySelector('.diagram-container') as any;
+    if (!container) return;
+
+    // get positions
+    const rect = container.getBoundingClientRect();
+    const centerX = rect.width / 2;
+    const centerY = rect.height / 2;
+    const beforeX = (centerX - panX) / zoomLevel;
+    const beforeY = (centerY - panY) / zoomLevel;
+
+    // apply zoom
+    const newZoom = Math.min(zoomLevel * ZOOM_BUTTON_FACTOR, MAX_ZOOM);
+    panX = centerX - beforeX * newZoom;
+    panY = centerY - beforeY * newZoom;
+    zoomLevel = newZoom;
+    applyTransform(document);
+}
+
+/**
+ * Zooms out the diagram
+ * @param document The document object
+ */
+export function zoomOut(document: any) {
+    const container = document.querySelector('.diagram-container') as any;
+    if (!container) return;
+
+    // get positions
+    const rect = container.getBoundingClientRect();
+    const centerX = rect.width / 2;
+    const centerY = rect.height / 2;
+    const beforeX = (centerX - panX) / zoomLevel;
+    const beforeY = (centerY - panY) / zoomLevel;
+
+    // apply zoom
+    const newZoom = Math.max(zoomLevel / ZOOM_BUTTON_FACTOR, MIN_ZOOM);
+    panX = centerX - beforeX * newZoom;
+    panY = centerY - beforeY * newZoom;
+    zoomLevel = newZoom;
+    applyTransform(document);
+}
+
+/**
+ * Resets zoom and pan to default values
+ * @param document The document object
+ */ 
+export function resetZoom(document: any) {
+    zoomLevel = 1;
+    panX = 0;
+    panY = 0;
+    applyTransform(document);
+}
+
+/**
+ * Applies the current zoom and pan transform to the diagram
+ * @param document The document object
+ */
+export function applyTransform(document: any) {
+    const wrapper = document.getElementById('diagram-wrapper');
+    if (!wrapper) return;
+    wrapper.style.transform = `matrix(${zoomLevel}, 0, 0, ${zoomLevel}, ${panX}, ${panY})`;
+
+}
+
+/**
+ * Sets up pan event listeners to move in the diagram
+ * @param document The document object
+ */
+export function registerPanListeners(document: any) {
+    const container = document.querySelector('.diagram-container') as any;
+    if (!container) return;
+
+    const onMouseDown = (e: any) => {
+        const target = e.target as any;
+        if (target.tagName === 'A' || target.tagName === 'BUTTON') return;
+
+        e.preventDefault();
+        isPanning = true;
+        startX = e.clientX - panX;
+        startY = e.clientY - panY;
+        container.style.cursor = 'grabbing';
+    };
+
+    const onMouseMove = (e: any) => {
+        if (!isPanning) return;
+        e.preventDefault();
+        panX = e.clientX - startX;
+        panY = e.clientY - startY;
+        applyTransform(document);
+    };
+
+    const onMouseUp = () => {
+        if (!isPanning) return;
+        isPanning = false;
+        container.style.cursor = 'grab';
+    };
+
+    const onMouseLeave = () => {
+       if (!isPanning) return;
+        isPanning = false;
+        container.style.cursor = 'grab';
+    };
+
+    const onWheel = (e: any) => {
+        e.preventDefault();
+
+        // get positions
+        const rect = container.getBoundingClientRect();
+        const mouseX = e.clientX - rect.left;
+        const mouseY = e.clientY - rect.top;
+        const beforeX = (mouseX - panX) / zoomLevel;
+        const beforeY = (mouseY - panY) / zoomLevel;
+
+        // apply zoom
+        const delta = e.deltaY > 0 ? SCROLL_ZOOM_OUT_FACTOR : SCROLL_ZOOM_IN_FACTOR;
+        const newZoom = Math.max(MIN_ZOOM, Math.min(MAX_ZOOM, zoomLevel * delta));
+        panX = mouseX - beforeX * newZoom;
+        panY = mouseY - beforeY * newZoom;
+        zoomLevel = newZoom;
+        applyTransform(document);
+    };
+
+    // add event listeners
+    container.addEventListener('mousedown', onMouseDown);
+    container.addEventListener('mouseleave', onMouseLeave);
+    document.addEventListener('mousemove', onMouseMove);
+    document.addEventListener('mouseup', onMouseUp);
+    container.addEventListener('wheel', onWheel, { passive: false });
+}

client/src/webview/script.ts

@@ -1,7 +1,7 @@
 import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/verification/derivation-nodes";
 import { renderLoading } from "./views/loading";
 import { renderStateMachineView } from "./views/diagram";
-import { createMermaidDiagram, renderMermaidDiagram } from "./mermaid";
+import { applyTransform, createMermaidDiagram, renderMermaidDiagram, resetZoom, registerPanListeners, zoomIn, zoomOut } from "./diagram";
 import type { LJDiagnostic } from "../types/diagnostics";
 import type { StateMachine } from "../types/fsm";
 import type { NavTab } from "./views/sections";
@@ -81,10 +81,32 @@ export function getScript(vscode: any, document: any, window: any) {
         if (target.id === 'diagram-orientation-btn') {
             e.stopPropagation();
             diagramOrientation = diagramOrientation === "TB" ? "LR" : "TB";
+            resetZoom(document);
             updateView();
             return;
         }
 
+        // zoom in
+        if (target.id === 'zoom-in-btn') {
+            e.stopPropagation();
+            zoomIn(document);
+            return;
+        }
+
+        // zoom out
+        if (target.id === 'zoom-out-btn') {
+            e.stopPropagation();
+            zoomOut(document);
+            return;
+        }
+
+        // reset zoom
+        if (target.id === 'zoom-reset-btn') {
+            e.stopPropagation();
+            resetZoom(document);
+            return;
+        }
+
         // toggle show more/less for errors
         if (target.classList.contains('show-more-button')) {
             e.stopPropagation();

client/src/webview/styles.ts

@@ -64,7 +64,7 @@ export function getStyles(): string {
         nav .selected {
             opacity: 1;
             text-decoration: underline;
-            text-decoration-color: #0078D5;
+            text-decoration-color: var(--vscode-activityBar-activeBorder);
             text-underline-offset: 6px;
             text-decoration-thickness: 1px;
         }
@@ -300,7 +300,23 @@ export function getStyles(): string {
             background-color: var(--vscode-editor-background);
             border-radius: 4px;
             padding: 1rem;
-            overflow-x: auto;
+            overflow: hidden;
+            position: relative;
+            cursor: grab;
+            user-select: none;
+        }
+        .diagram-container:active {
+            cursor: grabbing;
+        }
+        .diagram-wrapper {
+            transition: transform 0.1s ease-out;
+            transform-origin: 0 0;
+            display: inline-block;
+            min-width: 100%;
+            pointer-events: none;
+        }
+        .diagram-wrapper * {
+            pointer-events: auto;
         }
         .diagram-container .mermaid {
             display: flex;
@@ -310,8 +326,29 @@ export function getStyles(): string {
             max-width: 100%;
             height: auto;
         }
+        .diagram-controls {
+            position: absolute;
+            top: 0.5rem;
+            right: 0.5rem;
+            display: flex;
+            gap: 0.5rem;
+            z-index: 10;
+        }
+        .diagram-control-btn {
+            font-size: clamp(0.75rem, 5vw, 1.5rem);
+            padding: clamp(0.25rem, 1vw, 0.5rem);
+            color: var(--vscode-foreground);
+            background: none;
+            border: none;
+            font-family: 'Courier New', Courier, monospace;
+            opacity: 0.7;
+        }
+        .diagram-control-btn:hover {
+            background: none;
+            opacity: 1;
+        }
         .mermaid .statediagramTitleText {
-            font-size: 22px!important;
+            font-size: 30px!important;
         }
     `;
 }

client/src/webview/views/diagram.ts

@@ -7,11 +7,17 @@ export function renderStateMachineView(sm: StateMachine, diagram: string, select
             ${renderMainHeader("", selectedTab)}
             ${sm ? /*html*/`
                 <div class="diagram-section">
-                     <button id="diagram-orientation-btn" class="underline-button">
-                        ${orientation === "TB" ? `Show diagram horizontally` : `Show diagram vertically`}
-                    </button>
+
                     <div class="diagram-container">
-                        <pre class="mermaid">${diagram}</pre>
+                        <div class="diagram-controls">
+                            <button id="zoom-in-btn" class="diagram-control-btn" title="Zoom In">+</button>
+                            <button id="zoom-out-btn" class="diagram-control-btn" title="Zoom Out">-</button>
+                            <button id="zoom-reset-btn" class="diagram-control-btn" title="Reset Zoom">⟲</button>
+                            <button id="diagram-orientation-btn" class="diagram-control-btn" title="Rotate Diagram">${orientation === "TB" ? "↓" : "→"}</button>
+                        </div>
+                        <div id="diagram-wrapper" class="diagram-wrapper">
+                            <pre class="mermaid">${diagram}</pre>
+                        </div>
                     </div>
                     <div>
                         <p><strong>States:</strong> ${sm.states.join(', ')}</p>