diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts new file mode 100644 index 0000000..3878eee --- /dev/null +++ b/client/src/webview/diagram.ts @@ -0,0 +1,233 @@ +import type { StateMachine } from "../types/fsm"; + +// constants +const MIN_ZOOM = 0.2; +const MAX_ZOOM = 5; +const ZOOM_BUTTON_FACTOR = 1.5; +const SCROLL_ZOOM_IN_FACTOR = 1.05; +const SCROLL_ZOOM_OUT_FACTOR = 0.95; +const COPY_TIMEOUT_MS = 2000; + +// 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(); + 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 }); +} + +export async function copyDiagramToClipboard(target: any, diagram: string) { + const textContent = target.textContent; + const title = target.getAttribute('title'); + try { + target.disabled = true; + await navigator.clipboard.writeText(diagram); + target.textContent = '✓'; + target.setAttribute('title', 'Copied!'); + } catch (e) { + target.textContent = '✗'; + target.setAttribute('title', 'Copy failed'); + } finally { + // reset button after timeout + setTimeout(() => { + target.textContent = textContent; + target.setAttribute('title', title); + target.disabled = false; + }, COPY_TIMEOUT_MS); + } +} \ No newline at end of file diff --git a/client/src/webview/mermaid.ts b/client/src/webview/mermaid.ts deleted file mode 100644 index 2539cd0..0000000 --- a/client/src/webview/mermaid.ts +++ /dev/null @@ -1,55 +0,0 @@ -import type { StateMachine } from "../types/fsm"; - -/** - * 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(); - 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'); -} - -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 }); - } catch (e) { - console.error('Failed to render Mermaid diagram:', e); - } -} \ No newline at end of file diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 421972f..dfa4ff8 100644 --- a/client/src/webview/script.ts +++ b/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 { createMermaidDiagram, renderMermaidDiagram, resetZoom, registerPanListeners, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram"; import type { LJDiagnostic } from "../types/diagnostics"; import type { StateMachine } from "../types/fsm"; import type { NavTab } from "./views/sections"; @@ -22,6 +22,7 @@ export function getScript(vscode: any, document: any, window: any) { let stateMachine: StateMachine | undefined; let selectedTab: NavTab = 'verification'; let diagramOrientation: "LR" | "TB" = "TB"; + let currentDiagram: string = ''; // initial state root.innerHTML = renderLoading(); @@ -81,10 +82,40 @@ 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; + } + + // copy diagram source + if (target.id === 'copy-diagram-btn') { + e.stopPropagation(); + if (!currentDiagram) return + copyDiagramToClipboard(target, currentDiagram); + return; + } + // toggle show more/less for errors if (target.classList.contains('show-more-button')) { e.stopPropagation(); @@ -112,6 +143,7 @@ export function getScript(vscode: any, document: any, window: any) { } }); + // message event listener from extension window.addEventListener('message', event => { const msg = event.data; if (msg.type === 'diagnostics') { @@ -139,6 +171,7 @@ export function getScript(vscode: any, document: any, window: any) { root.innerHTML = renderVerificationView(diagnostics, showAllDiagnostics, currentFile, expandedErrors, selectedTab) } else { const diagram = createMermaidDiagram(stateMachine, diagramOrientation); + currentDiagram = diagram; root.innerHTML = renderStateMachineView(stateMachine, diagram, selectedTab, diagramOrientation); if (stateMachine) renderMermaidDiagram(document, window); } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index f5b94d3..f4d5797 100644 --- a/client/src/webview/styles.ts +++ b/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; } `; } \ No newline at end of file diff --git a/client/src/webview/views/diagram.ts b/client/src/webview/views/diagram.ts index 3937e89..a0374cf 100644 --- a/client/src/webview/views/diagram.ts +++ b/client/src/webview/views/diagram.ts @@ -7,11 +7,18 @@ export function renderStateMachineView(sm: StateMachine, diagram: string, select ${renderMainHeader("", selectedTab)} ${sm ? /*html*/`
- +
- 
${diagram}
+
+ + + + + +
+
+ 
${diagram}
+

States: ${sm.states.join(', ')}

diff --git a/client/tsconfig.json b/client/tsconfig.json index cf339d3..aa0e6fd 100644 --- a/client/tsconfig.json +++ b/client/tsconfig.json @@ -2,7 +2,7 @@ "compilerOptions": { "module": "commonjs", "target": "es2019", - "lib": ["ES2019"], + "lib": ["ES2019", "DOM"], "outDir": "out", "sourceMap": true, "rootDir": "src"