diff --git a/client/.vscodeignore b/client/.vscodeignore index c04789a..0f5bd73 100644 --- a/client/.vscodeignore +++ b/client/.vscodeignore @@ -11,6 +11,12 @@ vsc-extension-quickstart.md # Build artifacts out/** node_modules/** +!node_modules/ +!node_modules/@vscode/ +!node_modules/@vscode/codicons/ +!node_modules/@vscode/codicons/dist/ +!node_modules/@vscode/codicons/dist/codicon.css +!node_modules/@vscode/codicons/dist/codicon.ttf *.vsix # Test files diff --git a/client/package-lock.json b/client/package-lock.json index c40ab3c..bfd164f 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -9,6 +9,7 @@ "version": "0.0.78", "license": "MIT", "dependencies": { + "@vscode/codicons": "^0.0.45", "ftp": "^0.3.10", "get-port": "^5.1.1", "jsonc-parser": "^0.4.2", @@ -3212,9 +3213,20 @@ "engines": { "node": ">=0.10.0" } + }, + "node_modules/@vscode/codicons": { + "version": "0.0.45", + "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.45.tgz", + "integrity": "sha512-1KAZ7XCMagp5Gdrlr4bbbcAqgcIL623iO1wW6rfcSVGAVUQvR0WP7bQx1SbJ11gmV3fdQTSEFIJQ/5C+HuVasw==", + "license": "CC-BY-4.0" } }, "dependencies": { + "@vscode/codicons": { + "version": "0.0.45", + "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.45.tgz", + "integrity": "sha512-1KAZ7XCMagp5Gdrlr4bbbcAqgcIL623iO1wW6rfcSVGAVUQvR0WP7bQx1SbJ11gmV3fdQTSEFIJQ/5C+HuVasw==" + }, "@babel/code-frame": { "version": "7.12.11", "resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.12.11.tgz", diff --git a/client/package.json b/client/package.json index 3febc8e..da7ebae 100644 --- a/client/package.json +++ b/client/package.json @@ -178,6 +178,7 @@ "webpack-cli": "^5.1.4" }, "dependencies": { + "@vscode/codicons": "^0.0.45", "ftp": "^0.3.10", "get-port": "^5.1.1", "jsonc-parser": "^0.4.2", diff --git a/client/src/webview/clipboard.ts b/client/src/webview/clipboard.ts new file mode 100644 index 0000000..8a40025 --- /dev/null +++ b/client/src/webview/clipboard.ts @@ -0,0 +1,22 @@ +const COPY_BUTTON_RESET_MS = 2000; + +export async function copyToClipboard(button: HTMLButtonElement, text: string) { + const originalTitle = button.getAttribute('title'); + + try { + button.disabled = true; + await navigator.clipboard.writeText(text); + button.setAttribute('title', 'Copied!'); + } catch (e) { + button.setAttribute('title', 'Copy failed'); + } finally { + setTimeout(() => { + if (originalTitle !== null) { + button.setAttribute('title', originalTitle); + } else { + button.removeAttribute('title'); + } + button.disabled = false; + }, COPY_BUTTON_RESET_MS); + } +} diff --git a/client/src/webview/diagram.ts b/client/src/webview/diagram.ts index 19c6a7e..5683c02 100644 --- a/client/src/webview/diagram.ts +++ b/client/src/webview/diagram.ts @@ -1,4 +1,5 @@ import type { LJStateMachine } from "../types/fsm"; +import { copyToClipboard } from "./clipboard"; // constants const MIN_ZOOM = 0.2; @@ -6,7 +7,6 @@ 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; @@ -51,7 +51,7 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation // add transitions transitionMap.forEach((labels, key) => { const [from, to] = key.split('|'); - const mergedLabel = labels.join(', '); + const mergedLabel = labels.join('
'); lines.push(` ${from} --> ${to} : ${mergedLabel}`); }); @@ -59,10 +59,7 @@ export function createMermaidDiagram(sm: LJStateMachine | undefined, orientation } function getTransitionLabel(label: string, preCond?: string | null, postCond?: string | null, showConditions = false): string { - if (!showConditions) { - return escapeMermaidLabel(label); - } - + if (!showConditions) return escapeMermaidLabel(label); return [ getConditionLabel('pre', preCond), escapeMermaidLabel(label), @@ -75,9 +72,8 @@ function getInitialTransitionLabel(postCond?: string | null, showConditions = fa } function getConditionLabel(kind: 'pre' | 'post', cond?: string | null): string { - if (!cond) { - return ''; - } + if (!cond) return ''; + return `${escapeMermaidLabel(cond)}`; } @@ -101,6 +97,8 @@ export async function renderMermaidDiagram(document: any, window: any) { await mermaid.run({ nodes: mermaidElements }); applyTransform(document); registerPanListeners(document); + const diagramContainer = document.querySelector('.diagram-container') as HTMLElement | null; + if (diagramContainer) diagramContainer.style.minHeight = ''; } catch (e) { console.error('Failed to render Mermaid diagram:', e); } @@ -241,20 +239,5 @@ export function registerPanListeners(document: any) { } export async function copyDiagramToClipboard(target: any, diagram: string) { - const title = target.getAttribute('title'); - try { - target.disabled = true; - await navigator.clipboard.writeText(diagram); - target.classList.add('copied'); - target.setAttribute('title', 'Copied!'); - } catch (e) { - target.setAttribute('title', 'Copy failed'); - } finally { - // reset button after timeout - setTimeout(() => { - target.setAttribute('title', title); - target.classList.remove('copied'); - target.disabled = false; - }, COPY_TIMEOUT_MS); - } + await copyToClipboard(target, diagram); } diff --git a/client/src/webview/html.ts b/client/src/webview/html.ts index c878007..f444fb1 100644 --- a/client/src/webview/html.ts +++ b/client/src/webview/html.ts @@ -13,6 +13,7 @@ export function getHtml(webview: vscode.Webview, extensionUri: vscode.Uri): stri const nonce = Date.now().toString(); const cspSource = webview.cspSource; const scriptUri = webview.asWebviewUri(vscode.Uri.joinPath(extensionUri, "media", "webview.js")); + const codiconsUri = webview.asWebviewUri(vscode.Uri.joinPath(extensionUri, "node_modules", "@vscode", "codicons", "dist", "codicon.css")); return /*html*/ ` @@ -21,8 +22,9 @@ export function getHtml(webview: vscode.Webview, extensionUri: vscode.Uri): stri + diff --git a/client/src/webview/icons.ts b/client/src/webview/icons.ts new file mode 100644 index 0000000..367047b --- /dev/null +++ b/client/src/webview/icons.ts @@ -0,0 +1,23 @@ +export function renderCodicon(name: string, className = ""): string { + const classes = ["codicon", `codicon-${name}`, className].filter(Boolean).join(" "); + return ``; +} + +type CodiconButtonOptions = { + id?: string; + className?: string; + title: string; + ariaLabel?: string; + attributes?: string; + disabled?: boolean; +}; + +export function renderCodiconButton(iconName: string, options: CodiconButtonOptions): string { + const classes = ["icon-button", options.className].filter(Boolean).join(" "); + const id = options.id ? ` id="${options.id}"` : ""; + const ariaLabel = ` aria-label="${options.ariaLabel ?? options.title}"`; + const attributes = options.attributes ? ` ${options.attributes}` : ""; + const disabled = options.disabled ? " disabled" : ""; + + return `${renderCodicon(iconName)}`; +} diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index d017fdd..d48401d 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -54,6 +54,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) root.addEventListener('click', (e: MouseEvent) => { const target = e.target instanceof Element ? e.target : null; if (!target) return; + const iconButton = target.closest?.('.icon-button'); + if (iconButton && !(iconButton as HTMLButtonElement).disabled) { + iconButton.classList.remove('icon-button-pop'); + void (iconButton as HTMLElement).offsetWidth; + iconButton.classList.add('icon-button-pop'); + } // context section toggle const contextToggleButton = target.closest?.('.context-toggle-btn'); @@ -77,7 +83,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const icon = contextToggleButton.querySelector('.context-toggle-icon'); if (icon) { - icon.textContent = nextExpanded ? '▾' : '▸'; + icon.classList.toggle('codicon-triangle-down', nextExpanded); + icon.classList.toggle('codicon-triangle-right', !nextExpanded); } return; @@ -143,7 +150,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } // toggle diagram orientation - if (target.id === 'diagram-orientation-btn') { + if (target.closest?.('#diagram-orientation-btn')) { e.stopPropagation(); diagramOrientation = diagramOrientation === "TB" ? "LR" : "TB"; resetZoom(document); @@ -152,40 +159,42 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } // toggle diagram conditions - if (target.id === 'diagram-conditions-btn') { + const diagramConditionsButton = target.closest?.('#diagram-conditions-btn'); + if (diagramConditionsButton) { e.stopPropagation(); - if ((target as HTMLButtonElement).disabled) return; + if ((diagramConditionsButton as HTMLButtonElement).disabled) return; showDiagramConditions = !showDiagramConditions; updateView(); return; } // zoom in - if (target.id === 'zoom-in-btn') { + if (target.closest?.('#zoom-in-btn')) { e.stopPropagation(); zoomIn(document); return; } // zoom out - if (target.id === 'zoom-out-btn') { + if (target.closest?.('#zoom-out-btn')) { e.stopPropagation(); zoomOut(document); return; } // reset zoom - if (target.id === 'zoom-reset-btn') { + if (target.closest?.('#zoom-reset-btn')) { e.stopPropagation(); resetZoom(document); return; } // copy diagram source - if (target.id === 'copy-diagram-btn') { + const copyDiagramButton = target.closest?.('#copy-diagram-btn'); + if (copyDiagramButton) { e.stopPropagation(); if (!currentDiagram) return - copyDiagramToClipboard(target, currentDiagram); + copyDiagramToClipboard(copyDiagramButton, currentDiagram); return; } @@ -315,7 +324,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) case 'fsm': { const diagram = createMermaidDiagram(stateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; - root.innerHTML = renderStateMachineView(stateMachine, diagram, diagramOrientation, showDiagramConditions); + renderStateMachineView(root, stateMachine, diagram, diagramOrientation, showDiagramConditions); if (stateMachine) renderMermaidDiagram(document, window); break; } diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index a09bf13..d76c927 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -11,6 +11,7 @@ export function getStyles(): string { height: 100%; margin: 0; box-sizing: border-box; + scrollbar-gutter: stable both-edges; } #root { width: 100%; @@ -27,7 +28,8 @@ export function getStyles(): string { height: 100%; padding: 1rem; font-family: var(--vscode-font-family); - overflow: auto; + overflow-x: hidden; + overflow-y: auto; --lj-token-keyword: var(--vscode-symbolIcon-keywordForeground, var(--vscode-editor-foreground)); --lj-token-control: var(--vscode-debugTokenExpression-name, var(--vscode-symbolIcon-keywordForeground, var(--vscode-editor-foreground))); --lj-token-function: var(--vscode-symbolIcon-functionForeground, var(--vscode-editor-foreground)); @@ -38,7 +40,7 @@ export function getStyles(): string { --lj-token-boolean: var(--vscode-debugTokenExpression-boolean, var(--vscode-symbolIcon-booleanForeground, var(--vscode-editor-foreground))); --lj-token-identifier: var(--vscode-debugTokenExpression-name, var(--vscode-editor-foreground)); --lj-token-punctuation: var(--vscode-editor-foreground); - --lj-state-cond-pre: var(--lj-token-function); + --lj-state-cond-pre: var(--lj-token-identifier); --lj-state-cond-post: var(--lj-token-type); } body.vscode-light { @@ -164,6 +166,16 @@ export function getStyles(): string { border-radius: 4px; position: relative; } + .codicon { + display: inline-flex; + align-items: center; + justify-content: center; + width: 1em; + height: 1em; + font-size: 1rem; + line-height: 1; + pointer-events: none; + } .copy-diagnostic-btn { position: absolute; top: 0.5rem; @@ -179,7 +191,6 @@ export function getStyles(): string { border: 1px solid transparent; border-radius: 4px; opacity: 0.65; - font-size: 1.25rem; transition: background-color 0.16s ease, border-color 0.16s ease, opacity 0.16s ease, transform 0.16s ease; } .copy-diagnostic-btn:hover { @@ -191,15 +202,15 @@ export function getStyles(): string { opacity: 0.8; cursor: default; } - .copied { - animation: copy-diagnostic-pop 0.42s ease-out; + .icon-button-pop { + animation: icon-button-pop 0.28s ease-out; } - @keyframes copy-diagnostic-pop { + @keyframes icon-button-pop { 0% { - transform: scale(0.8); + transform: scale(0.96); } - 45% { - transform: scale(1.18); + 55% { + transform: scale(1.05); } 100% { transform: scale(1); @@ -328,14 +339,18 @@ export function getStyles(): string { } .reset-btn { margin: 0; - padding: 0.4rem 0.8rem; + display: inline-flex; + align-items: center; + justify-content: center; + width: 1.75rem; + height: 1.75rem; + padding: 0; background-color: transparent; color: var(--vscode-button-foreground); border: none; border-radius: 4px; cursor: pointer; font-family: var(--vscode-font-family); - font-size: larger; flex-shrink: 0; opacity: 0.7; } @@ -560,7 +575,6 @@ export function getStyles(): string { width: 1rem; text-align: center; flex-shrink: 0; - font-size: larger; } .context-section-content.collapsed { display: none; @@ -633,19 +647,40 @@ export function getStyles(): string { } .diagram-controls { position: absolute; - top: 0.5rem; - right: 0.5rem; + top: 1rem; + right: 1rem; display: flex; gap: 0.5rem; z-index: 10; } + .diagram-condition-legend { + position: absolute; + bottom: 1rem; + right: 1rem; + display: flex; + flex-direction: column; + gap: 0.25rem; + font-size: 0.8rem; + z-index: 10; + pointer-events: none; + font-weight: 500; + } + .diagram-condition-legend-pre { + color: var(--lj-state-cond-pre); + } + .diagram-condition-legend-post { + color: var(--lj-state-cond-post); + } .diagram-control-btn { - font-size: clamp(0.75rem, 5vw, 1.5rem); - padding: clamp(0.25rem, 1vw, 0.5rem); + display: inline-flex; + align-items: center; + justify-content: center; + width: 1.75rem; + height: 1.75rem; + padding: 0; color: var(--vscode-foreground); background: none; border: none; - font-family: 'Courier New', Courier, monospace; opacity: 0.7; } .diagram-control-btn:hover { @@ -689,7 +724,7 @@ export function getStyles(): string { .diagram-container .mermaid .edgeLabel .state-cond { color: var(--vscode-descriptionForeground) !important; display: inline-block !important; - font-size: 0.82em !important; + font-size: 0.76em !important; line-height: 1.2 !important; } .diagram-container .mermaid .edgeLabel .state-cond-pre { diff --git a/client/src/webview/views/diagnostics/derivation-nodes.ts b/client/src/webview/views/diagnostics/derivation-nodes.ts index ca8e8a3..8a75964 100644 --- a/client/src/webview/views/diagnostics/derivation-nodes.ts +++ b/client/src/webview/views/diagnostics/derivation-nodes.ts @@ -1,6 +1,7 @@ import type { LJError, RefinementMismatchError } from "../../../types/diagnostics"; import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; import { escapeHtml } from "../../utils"; // Handles rendering and interaction of derivation nodes in refinement errors @@ -138,7 +139,7 @@ export function renderDerivationNode( ${renderJsonTree(error, node, errorId, "root", expansions)} ${expansions.size === 0 ? ' (click to expand)' : ''} - + `; } diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index 8895cdf..f0b4232 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -1,10 +1,10 @@ import { LJDiagnostic, LJError, LJWarning } from "../../../types/diagnostics"; +import { copyToClipboard } from "../../clipboard"; +import { renderCodiconButton } from "../../icons"; import { renderErrors } from "./errors"; import { renderMainHeader } from "../sections"; import { renderWarnings } from "./warnings"; -const COPY_BUTTON_RESET_MS = 2000; - export function renderDiagnosticsView( diagnostics: LJDiagnostic[], showAll: boolean, @@ -51,7 +51,11 @@ export function getDisplayDiagnostics(diagnostics: LJDiagnostic[], showAll: bool } export function renderCopyDiagnosticButton(indexType: 'error' | 'warning', index: number): string { - return /*html*/``; + return renderCodiconButton("copy", { + className: "copy-diagnostic-btn", + title: "Copy diagnostic", + attributes: `data-${indexType}-index="${index}"`, + }); } export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: LJDiagnostic[]) { @@ -63,24 +67,7 @@ export async function copyDiagnosticToClipboard(button: any, displayDiagnostics: if (!diagnostic) return; const diagnosticText = formatDiagnosticForClipboard(diagnostic); - const originalTitle = button.getAttribute('title'); - const originalContent = button.innerHTML; - - try { - button.disabled = true; - await navigator.clipboard.writeText(diagnosticText); - button.classList.add('copied'); - button.setAttribute('title', 'Copied!'); - } catch (e) { - button.setAttribute('title', 'Copy failed'); - } finally { - setTimeout(() => { - button.innerHTML = originalContent; - button.setAttribute('title', originalTitle); - button.classList.remove('copied'); - button.disabled = false; - }, COPY_BUTTON_RESET_MS); - } + await copyToClipboard(button, diagnosticText); } export function formatDiagnosticForClipboard(diagnostic: LJDiagnostic): string { diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index bf10010..3080baa 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -1,29 +1,41 @@ import type { LJStateMachine } from "../../../types/fsm"; +import { renderCodiconButton } from "../../icons"; import { renderMainHeader } from "../sections"; -export function renderStateMachineView(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean): string { +export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean) { + const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; + const diagramHeight = previousDiagramContainer?.offsetHeight; + root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight); +} + +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number): string { const initialStateNames = sm ? [...new Set(sm.initialTransitions.map(transition => transition.to))] : []; const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.postCond) || sm.transitions.some(transition => !!transition.preCond || !!transition.postCond) : false; const conditionToggleLabel = showConditions ? 'Collapse Conditions' : 'Expand Conditions'; - const conditionToggleIcon = showConditions ? '⊟' : '⊞'; return /*html*/`
${renderMainHeader("", 'fsm')} ${sm ? /*html*/`
-
+
- - - - - - + ${renderCodiconButton("zoom-in", { id: "zoom-in-btn", className: "diagram-control-btn", title: "Zoom In" })} + ${renderCodiconButton("zoom-out", { id: "zoom-out-btn", className: "diagram-control-btn", title: "Zoom Out" })} + ${renderCodiconButton("screen-normal", { id: "zoom-reset-btn", className: "diagram-control-btn", title: "Reset Zoom" })} + ${renderCodiconButton(orientation === "TB" ? "arrow-down" : "arrow-right", { id: "diagram-orientation-btn", className: "diagram-control-btn", title: "Toggle Orientation" })} + ${renderCodiconButton(showConditions ? "collapse-all" : "expand-all", { id: "diagram-conditions-btn", className: `diagram-control-btn${showConditions ? ' active' : ''}`, title: conditionToggleLabel, attributes: `aria-pressed="${showConditions ? 'true' : 'false'}"`, disabled: !hasConditionExpansions })} + ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
+ ${showConditions && hasConditionExpansions ? /*html*/` +
+ Precondition + Postcondition +
+ ` : ''} 
${diagram}
diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index 0ce66fe..3b13934 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -2,6 +2,7 @@ import type { LJDiagnostic, PlacementInCode, SourcePosition, TranslationTable } import { escapeHtml } from "../utils"; import { renderHighlightedExpression, renderHighlightedInlineExpression } from "../highlighting"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diagnostic-reveal"; +import { renderCodicon } from "../icons"; export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
@@ -21,7 +22,7 @@ export const renderExpressionSection = (title: string, expression: string): stri export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/` `;