Skip to content

Commit 3d54731

Browse files
rcosta358rcosta358
authored
Add Zoom & Move Controls to Diagram (#53)
1 parent 968d05a commit 3d54731

File tree

6 files changed

+319
-64
lines changed

6 files changed

+319
-64
lines changed

‎client/src/webview/diagram.ts‎

Lines changed: 233 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,233 @@
1+
import type { StateMachine } from "../types/fsm";
2+
3+
// constants
4+
const MIN_ZOOM = 0.2;
5+
const MAX_ZOOM = 5;
6+
const ZOOM_BUTTON_FACTOR = 1.5;
7+
const SCROLL_ZOOM_IN_FACTOR = 1.05;
8+
const SCROLL_ZOOM_OUT_FACTOR = 0.95;
9+
const COPY_TIMEOUT_MS = 2000;
10+
11+
// state variables
12+
let zoomLevel = 1;
13+
let panX = 0;
14+
let panY = 0;
15+
let isPanning = false;
16+
let startX = 0;
17+
let startY = 0;
18+
19+
/**
20+
* Converts a StateMachine object to a Mermaid state diagram string
21+
* @param sm
22+
* @returns Mermaid diagram string
23+
*/
24+
export function createMermaidDiagram(sm: StateMachine, orientation: "LR" | "TB"): string {
25+
if (!sm) return '';
26+
27+
const lines: string[] = [];
28+
29+
// header
30+
lines.push('---');
31+
lines.push(`title: ${sm.className}`);
32+
lines.push('---');
33+
lines.push('stateDiagram-v2');
34+
lines.push(` direction ${orientation}`);
35+
36+
// initial states
37+
sm.initialStates.forEach(state => {
38+
lines.push(` [*] --> ${state}`);
39+
});
40+
41+
// group transitions by from/to states and merge labels
42+
const transitionMap = new Map<string, string[]>();
43+
sm.transitions.forEach(transition => {
44+
const key = `${transition.from}|${transition.to}`;
45+
if (!transitionMap.has(key)) transitionMap.set(key, []);
46+
transitionMap.get(key).push(transition.label);
47+
});
48+
49+
// add transitions
50+
transitionMap.forEach((labels, key) => {
51+
const [from, to] = key.split('|');
52+
const mergedLabel = labels.join(', ');
53+
lines.push(` ${from} --> ${to} : ${mergedLabel}`);
54+
});
55+
56+
return lines.join('\n');
57+
}
58+
59+
/**
60+
* Renders Mermaid diagrams in the document
61+
* @param document The document object
62+
* @param window The window object
63+
*/
64+
export async function renderMermaidDiagram(document: any, window: any) {
65+
const mermaid = (window as any).mermaid;
66+
if (!mermaid) return;
67+
68+
const mermaidElements = document.querySelectorAll('.mermaid');
69+
if (mermaidElements.length === 0) return;
70+
71+
try {
72+
await mermaid.run({ nodes: mermaidElements });
73+
applyTransform(document);
74+
registerPanListeners(document);
75+
} catch (e) {
76+
console.error('Failed to render Mermaid diagram:', e);
77+
}
78+
}
79+
80+
/**
81+
* Resets zoom and pan to default values
82+
* @param document The document object
83+
*/
84+
export function zoomIn(document: any) {
85+
const container = document.querySelector('.diagram-container') as any;
86+
if (!container) return;
87+
88+
// get positions
89+
const rect = container.getBoundingClientRect();
90+
const centerX = rect.width / 2;
91+
const centerY = rect.height / 2;
92+
const beforeX = (centerX - panX) / zoomLevel;
93+
const beforeY = (centerY - panY) / zoomLevel;
94+
95+
// apply zoom
96+
const newZoom = Math.min(zoomLevel * ZOOM_BUTTON_FACTOR, MAX_ZOOM);
97+
panX = centerX - beforeX * newZoom;
98+
panY = centerY - beforeY * newZoom;
99+
zoomLevel = newZoom;
100+
applyTransform(document);
101+
}
102+
103+
/**
104+
* Zooms out the diagram
105+
* @param document The document object
106+
*/
107+
export function zoomOut(document: any) {
108+
const container = document.querySelector('.diagram-container') as any;
109+
if (!container) return;
110+
111+
// get positions
112+
const rect = container.getBoundingClientRect();
113+
const centerX = rect.width / 2;
114+
const centerY = rect.height / 2;
115+
const beforeX = (centerX - panX) / zoomLevel;
116+
const beforeY = (centerY - panY) / zoomLevel;
117+
118+
// apply zoom
119+
const newZoom = Math.max(zoomLevel / ZOOM_BUTTON_FACTOR, MIN_ZOOM);
120+
panX = centerX - beforeX * newZoom;
121+
panY = centerY - beforeY * newZoom;
122+
zoomLevel = newZoom;
123+
applyTransform(document);
124+
}
125+
126+
/**
127+
* Resets zoom and pan to default values
128+
* @param document The document object
129+
*/
130+
export function resetZoom(document: any) {
131+
zoomLevel = 1;
132+
panX = 0;
133+
panY = 0;
134+
applyTransform(document);
135+
}
136+
137+
/**
138+
* Applies the current zoom and pan transform to the diagram
139+
* @param document The document object
140+
*/
141+
export function applyTransform(document: any) {
142+
const wrapper = document.getElementById('diagram-wrapper');
143+
if (!wrapper) return;
144+
wrapper.style.transform = `matrix(${zoomLevel}, 0, 0, ${zoomLevel}, ${panX}, ${panY})`;
145+
146+
}
147+
148+
/**
149+
* Sets up pan event listeners to move in the diagram
150+
* @param document The document object
151+
*/
152+
export function registerPanListeners(document: any) {
153+
const container = document.querySelector('.diagram-container') as any;
154+
if (!container) return;
155+
156+
const onMouseDown = (e: any) => {
157+
const target = e.target as any;
158+
if (target.tagName === 'A' || target.tagName === 'BUTTON') return;
159+
160+
e.preventDefault();
161+
isPanning = true;
162+
startX = e.clientX - panX;
163+
startY = e.clientY - panY;
164+
container.style.cursor = 'grabbing';
165+
};
166+
167+
const onMouseMove = (e: any) => {
168+
if (!isPanning) return;
169+
e.preventDefault();
170+
panX = e.clientX - startX;
171+
panY = e.clientY - startY;
172+
applyTransform(document);
173+
};
174+
175+
const onMouseUp = () => {
176+
if (!isPanning) return;
177+
isPanning = false;
178+
container.style.cursor = 'grab';
179+
};
180+
181+
const onMouseLeave = () => {
182+
if (!isPanning) return;
183+
isPanning = false;
184+
container.style.cursor = 'grab';
185+
};
186+
187+
const onWheel = (e: any) => {
188+
e.preventDefault();
189+
190+
// get positions
191+
const rect = container.getBoundingClientRect();
192+
const mouseX = e.clientX - rect.left;
193+
const mouseY = e.clientY - rect.top;
194+
const beforeX = (mouseX - panX) / zoomLevel;
195+
const beforeY = (mouseY - panY) / zoomLevel;
196+
197+
// apply zoom
198+
const delta = e.deltaY > 0 ? SCROLL_ZOOM_OUT_FACTOR : SCROLL_ZOOM_IN_FACTOR;
199+
const newZoom = Math.max(MIN_ZOOM, Math.min(MAX_ZOOM, zoomLevel * delta));
200+
panX = mouseX - beforeX * newZoom;
201+
panY = mouseY - beforeY * newZoom;
202+
zoomLevel = newZoom;
203+
applyTransform(document);
204+
};
205+
206+
// add event listeners
207+
container.addEventListener('mousedown', onMouseDown);
208+
container.addEventListener('mouseleave', onMouseLeave);
209+
document.addEventListener('mousemove', onMouseMove);
210+
document.addEventListener('mouseup', onMouseUp);
211+
container.addEventListener('wheel', onWheel, { passive: false });
212+
}
213+
214+
export async function copyDiagramToClipboard(target: any, diagram: string) {
215+
const textContent = target.textContent;
216+
const title = target.getAttribute('title');
217+
try {
218+
target.disabled = true;
219+
await navigator.clipboard.writeText(diagram);
220+
target.textContent = '✓';
221+
target.setAttribute('title', 'Copied!');
222+
} catch (e) {
223+
target.textContent = '✗';
224+
target.setAttribute('title', 'Copy failed');
225+
} finally {
226+
// reset button after timeout
227+
setTimeout(() => {
228+
target.textContent = textContent;
229+
target.setAttribute('title', title);
230+
target.disabled = false;
231+
}, COPY_TIMEOUT_MS);
232+
}
233+
}

‎client/src/webview/mermaid.ts‎

Lines changed: 0 additions & 55 deletions
This file was deleted.

‎client/src/webview/script.ts‎

Lines changed: 34 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/verification/derivation-nodes";
22
import { renderLoading } from "./views/loading";
33
import { renderStateMachineView } from "./views/diagram";
4-
import { createMermaidDiagram, renderMermaidDiagram } from "./mermaid";
4+
import { createMermaidDiagram, renderMermaidDiagram, resetZoom, registerPanListeners, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram";
55
import type { LJDiagnostic } from "../types/diagnostics";
66
import type { StateMachine } from "../types/fsm";
77
import type { NavTab } from "./views/sections";
@@ -22,6 +22,7 @@ export function getScript(vscode: any, document: any, window: any) {
2222
let stateMachine: StateMachine | undefined;
2323
let selectedTab: NavTab = 'verification';
2424
let diagramOrientation: "LR" | "TB" = "TB";
25+
let currentDiagram: string = '';
2526

2627
// initial state
2728
root.innerHTML = renderLoading();
@@ -81,10 +82,40 @@ export function getScript(vscode: any, document: any, window: any) {
8182
if (target.id === 'diagram-orientation-btn') {
8283
e.stopPropagation();
8384
diagramOrientation = diagramOrientation === "TB" ? "LR" : "TB";
85+
resetZoom(document);
8486
updateView();
8587
return;
8688
}
8789

90+
// zoom in
91+
if (target.id === 'zoom-in-btn') {
92+
e.stopPropagation();
93+
zoomIn(document);
94+
return;
95+
}
96+
97+
// zoom out
98+
if (target.id === 'zoom-out-btn') {
99+
e.stopPropagation();
100+
zoomOut(document);
101+
return;
102+
}
103+
104+
// reset zoom
105+
if (target.id === 'zoom-reset-btn') {
106+
e.stopPropagation();
107+
resetZoom(document);
108+
return;
109+
}
110+
111+
// copy diagram source
112+
if (target.id === 'copy-diagram-btn') {
113+
e.stopPropagation();
114+
if (!currentDiagram) return
115+
copyDiagramToClipboard(target, currentDiagram);
116+
return;
117+
}
118+
88119
// toggle show more/less for errors
89120
if (target.classList.contains('show-more-button')) {
90121
e.stopPropagation();
@@ -112,6 +143,7 @@ export function getScript(vscode: any, document: any, window: any) {
112143
}
113144
});
114145

146+
// message event listener from extension
115147
window.addEventListener('message', event => {
116148
const msg = event.data;
117149
if (msg.type === 'diagnostics') {
@@ -139,6 +171,7 @@ export function getScript(vscode: any, document: any, window: any) {
139171
root.innerHTML = renderVerificationView(diagnostics, showAllDiagnostics, currentFile, expandedErrors, selectedTab)
140172
} else {
141173
const diagram = createMermaidDiagram(stateMachine, diagramOrientation);
174+
currentDiagram = diagram;
142175
root.innerHTML = renderStateMachineView(stateMachine, diagram, selectedTab, diagramOrientation);
143176
if (stateMachine) renderMermaidDiagram(document, window);
144177
}

0 commit comments

Comments
 (0)