From de2c9c449ba54434f0a589891f07f3d716056329 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 20 Oct 2026 23:46:08 +0100 Subject: [PATCH 1/4] Show state errors beside the state machine diagram List the state refinement errors of the displayed machine next to the diagram, matched by class so errors reported in caller files appear on the machine from the refinements file. Each item shows the call, receiver, found and required states (from the extended error context when available, otherwise the diagnostic text) and links to its source. Selecting an item reuses the existing "View error on state machine" selection, clearing it restores the general diagram, and the selection is kept across verifications while its error still exists. Co-Authored-By: Claude Opus 5.5 --- client/src/test/state-errors.test.ts | 58 +++++++ client/src/types/fsm.ts | 5 + client/src/webview/script.spec.ts | 142 +++++++++++++++- client/src/webview/script.ts | 74 +++++++-- client/src/webview/styles.ts | 89 ++++++++++ client/src/webview/views/fsm/fsm.ts | 10 +- .../webview/views/fsm/state-errors.spec.ts | 144 ++++++++++++++++ client/src/webview/views/fsm/state-errors.ts | 156 ++++++++++++++++++ .../src/main/java/FailingTreeNodeState.java | 11 ++ .../src/main/java/TreeNodeRefinements.java | 22 +++ 10 files changed, 691 insertions(+), 20 deletions(-) create mode 100644 client/src/test/state-errors.test.ts create mode 100644 client/src/webview/views/fsm/state-errors.spec.ts create mode 100644 client/src/webview/views/fsm/state-errors.ts create mode 100644 client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java create mode 100644 client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java diff --git a/client/src/test/state-errors.test.ts b/client/src/test/state-errors.test.ts new file mode 100644 index 0000000..c6aff26 --- /dev/null +++ b/client/src/test/state-errors.test.ts @@ -0,0 +1,58 @@ +import * as assert from 'node:assert/strict'; +import * as path from 'node:path'; +import * as vscode from 'vscode'; +import type { LJDiagnostic, StateRefinementError } from '../types/diagnostics'; +import type { LJStateMachine } from '../types/fsm'; +import type { LiquidJavaTestApi } from '../types/test-api'; + +suite('Bundled LiquidJava state machine errors', () => { + test('sends state errors from the caller file with the machine of the refinements file', async () => { + const installed = vscode.extensions.getExtension('AlcidesFonseca.liquid-java'); + assert.ok(installed); + const api = await installed.activate(); + await api.ready; + + const workspace = vscode.workspace.workspaceFolders?.[0]; + assert.ok(workspace); + const refinementsUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/TreeNodeRefinements.java'); + const callerUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/FailingTreeNodeState.java'); + const sameFile = (file: string, uri: vscode.Uri) => vscode.Uri.file(path.resolve(file)).fsPath === uri.fsPath; + const subscriptions: vscode.Disposable[] = []; + const isStateError = (diagnostic: LJDiagnostic): diagnostic is StateRefinementError => + diagnostic.type === 'state-refinement-error' && sameFile(diagnostic.file, callerUri); + + try { + const ready = new Promise(resolve => subscriptions.push(api.onWebviewMessage(event => { + if (event.direction === 'fromWebview' && event.message.type === 'ready') resolve(); + }))); + await vscode.commands.executeCommand('liquidjava.showView'); + await Promise.race([ready, new Promise(resolve => setTimeout(resolve, 5000))]); + + const machine = new Promise(resolve => subscriptions.push(api.onWebviewMessage(event => { + if (event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm) resolve(event.message.sm); + }))); + const diagnostics = new Promise((resolve, reject) => { + subscriptions.push(api.onDiagnostics(value => { + if (value.some(isStateError)) resolve(value); + })); + subscriptions.push(api.onFailure(() => reject(new Error('LiquidJava verifier crashed while checking state errors')))); + }); + const document = await vscode.workspace.openTextDocument(refinementsUri); + await vscode.window.showTextDocument(document); + await vscode.commands.executeCommand('liquidjava.verify'); + + const [sm, result] = await Promise.all([machine, diagnostics]); + const error = result.find(isStateError); + assert.ok(error, JSON.stringify(result)); + assert.equal(sm.className, 'javax.swing.tree.DefaultMutableTreeNode'); + assert.ok(error.stateMachine, 'the state error must carry its state machine'); + assert.equal(error.stateMachine.className, sm.className, 'errors are matched to the machine by class'); + assert.ok(error.stateMachine.errorContext, 'the state error must carry its error context'); + assert.ok(error.position && sameFile(error.position.file ?? error.file, callerUri)); + assert.ok(error.declarationPosition?.file && sameFile(error.declarationPosition.file, refinementsUri)); + } finally { + subscriptions.forEach(subscription => subscription.dispose()); + await vscode.commands.executeCommand('workbench.action.closeAllEditors'); + } + }); +}); diff --git a/client/src/types/fsm.ts b/client/src/types/fsm.ts index 0d252ec..1003955 100644 --- a/client/src/types/fsm.ts +++ b/client/src/types/fsm.ts @@ -11,4 +11,9 @@ export type LJStateMachine = { export type LJStateMachineErrorContext = { calledMethod: string | null; actualStates: string[]; + receiver?: string | null; + expectedStates?: string[]; + expectedCondition?: string | null; + foundCondition?: string | null; + definiteFoundState?: string | null; }; diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index 25dfdca..b7d4053 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -1,7 +1,7 @@ import { JSDOM } from 'jsdom'; import { afterEach, beforeEach, describe, expect, it, vi, type Mock } from 'vitest'; import type { LJContext, LJVariable } from '../types/context'; -import type { LJDiagnostic, SourcePosition } from '../types/diagnostics'; +import type { LJDiagnostic, SourcePosition, StateRefinementError } from '../types/diagnostics'; import type { LJStateMachine } from '../types/fsm'; const currentFile = '/workspace/src/Main.java'; @@ -57,6 +57,36 @@ const stateMachine: LJStateMachine = { errorContext: null, }; +const refinementsFile = '/workspace/src/DefaultMutableTreeNodeRefinements.java'; +const treeMachine: LJStateMachine = { + className: 'javax.swing.tree.DefaultMutableTreeNode', + initialTransitions: [{ to: 'childrenAllowed' }], + states: ['childrenAllowed', 'maybeHasChildren'], + transitions: [ + { from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }, + { from: 'maybeHasChildren', to: 'childrenAllowed', label: 'removeAllChildren' }, + { from: 'maybeHasChildren', to: 'maybeHasChildren', label: 'getFirstChild' }, + ], + errorContext: null, +}; + +// state errors are reported in the caller file, while the machine comes from the refinements file +function stateError(line: number, calledMethod: string, receiver: string): StateRefinementError { + return { + category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', + message: `found childrenAllowed(${receiver}) but expected maybeHasChildren(${receiver})`, hint: null, + file: otherFile, position: { file: otherFile, lineStart: line, colStart: 8, lineEnd: line, colEnd: 30 }, + translationTable: {}, expected: `maybeHasChildren(${receiver})`, + found: { implication: { name: receiver, type: 'DefaultMutableTreeNode', predicate: `childrenAllowed(${receiver})`, next: null }, origin: null, simplification: null }, + customMessage: '', + declarationPosition: { file: refinementsFile, lineStart: calledMethod === 'getFirstChild' ? 21 : 18, colStart: 4, lineEnd: 21, colEnd: 40 }, + stateMachine: { ...treeMachine, errorContext: { + calledMethod, actualStates: ['childrenAllowed'], receiver, + expectedStates: ['maybeHasChildren'], definiteFoundState: 'childrenAllowed', + } }, + }; +} + describe('webview script', () => { let dom: JSDOM; let root: HTMLElement; @@ -226,4 +256,114 @@ describe('webview script', () => { highlightRange: range, }]]); }); + + describe('state errors beside the diagram', () => { + const firstChildError = stateError(10, 'getFirstChild', 'root'); + const removeError = stateError(15, 'removeAllChildren', 'menu'); + + function showStateMachine(diagnostics: LJDiagnostic[]) { + receive({ type: 'file', file: refinementsFile }); + receive({ type: 'diagnostics', diagnostics }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: treeMachine }); + click('[data-tab="fsm"]'); + } + + const items = () => Array.from(root.querySelectorAll('.state-error-select')); + const pressed = () => items().map(item => item.getAttribute('aria-pressed')); + const calls = () => Array.from(root.querySelectorAll('.state-error-call'), node => node.textContent); + const mermaidSource = () => root.querySelector('.mermaid')?.innerHTML ?? ''; + + it('lists errors from other files for the machine of the current file', () => { + showStateMachine([firstChildError, removeError, diagnostic(currentFile, 'Unrelated error')]); + + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('selects an error to highlight it and clears the selection to show the general diagram', () => { + showStateMachine([firstChildError, removeError]); + + items()[0].click(); + expect(pressed()).toEqual(['true', 'false']); + expect(mermaidSource()).toContain('class childrenAllowed ljStateErrorActual'); + expect(mermaidSource()).toContain('lj-state-error-method">getFirstChild'); + expect(dom.window.document.activeElement).toBe(items()[0]); + + items()[1].click(); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + expect(mermaidSource()).not.toContain('lj-state-error-method">getFirstChild'); + + // selecting the selected error again clears the selection + items()[1].click(); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + + items()[0].click(); + click('#state-error-clear-btn'); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + expect(root.querySelector('#state-error-clear-btn')?.disabled).toBe(true); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + }); + + it('keeps the selection when its error remains after verification and drops fixed errors', () => { + showStateMachine([firstChildError, removeError]); + items()[1].click(); + + receive({ type: 'diagnostics', diagnostics: [stateError(10, 'getFirstChild', 'root'), stateError(15, 'removeAllChildren', 'menu')] }); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + + receive({ type: 'diagnostics', diagnostics: [stateError(15, 'removeAllChildren', 'menu')] }); + expect(calls()).toEqual(['menu.removeAllChildren()']); + expect(pressed()).toEqual(['true']); + + receive({ type: 'diagnostics', diagnostics: [firstChildError] }); + expect(calls()).toEqual(['root.getFirstChild()']); + expect(pressed()).toEqual(['false']); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('keeps the diagram and drops the list once every state error is fixed', () => { + showStateMachine([firstChildError]); + items()[0].click(); + + receive({ type: 'diagnostics', diagnostics: [] }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(root.querySelector('.state-errors')).toBeNull(); + expect(root.querySelector('.fsm-layout')).toBeNull(); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('preselects the error opened with View error on state machine', () => { + receive({ type: 'file', file: otherFile }); + receive({ type: 'diagnostics', diagnostics: [firstChildError, removeError] }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: null }); + + root.querySelectorAll('.diagnostic-state-machine-btn')[1].click(); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('fsm'); + expect(calls()).toEqual(['root.getFirstChild()', 'menu.removeAllChildren()']); + expect(pressed()).toEqual(['false', 'true']); + expect(mermaidSource()).toContain('lj-state-error-method">removeAllChildren'); + + // the caller file has no machine of its own, so clearing keeps the error machine without its context + click('#state-error-clear-btn'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(pressed()).toEqual(['false', 'false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + }); + + it('leaves the view unchanged when the machine has no state errors', () => { + showStateMachine([diagnostic(currentFile, 'Unrelated error')]); + + expect(root.querySelector('.diagram-title')?.textContent).toBe('javax.swing.tree.DefaultMutableTreeNode'); + expect(root.querySelector('.state-errors')).toBeNull(); + expect(root.querySelector('.fsm-layout')).toBeNull(); + }); + }); }); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 05b6ed0..2052b69 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -3,7 +3,7 @@ import { renderLoading } from "./views/loading"; import { renderStopped } from "./views/stopped"; import { renderStateMachineView } from "./views/fsm/fsm"; import { createMermaidDiagram, renderMermaidDiagram, resetZoom, zoomIn, zoomOut, copyDiagramToClipboard } from "./diagram"; -import type { LJDiagnostic, RefinementMismatchError } from "../types/diagnostics"; +import type { LJDiagnostic, RefinementMismatchError, StateRefinementError } from "../types/diagnostics"; import type { Range } from "../types/context"; import type { LJStateMachine } from "../types/fsm"; import type { ExtensionStatus } from "../state"; @@ -13,6 +13,7 @@ import type { LJContext } from "../types/context"; import { ContextSectionState, renderContextView } from "./views/context/context"; import type { DiagnosticRevealTarget } from "../types/diagnostics"; import { getDiagnosticRevealTargetFromKey, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; +import { findStateError, focusStateError, getStateErrorKey, getStateMachineErrors, renderStateErrorList } from "./views/fsm/state-errors"; type VSCodeApi = { postMessage(message: unknown): void; @@ -33,6 +34,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let stateMachine: LJStateMachine | undefined; let diagnosticStateMachine: LJStateMachine | undefined; let diagnosticStateMachineFile: string | undefined; + let diagnosticStateMachineError: StateRefinementError | undefined; let context: LJContext; let errorAtCursor: RefinementMismatchError; let selectedTab: NavTab = 'diagnostics'; @@ -144,11 +146,28 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (diagnostic?.type !== 'state-refinement-error' || !diagnostic.stateMachine) return; selectedTab = 'fsm'; - diagnosticStateMachine = diagnostic.stateMachine; - diagnosticStateMachineFile = diagnostic.file; showDiagramConditions = false; - currentDiagram = ''; - updateView(); + selectStateError(diagnostic); + return; + } + + // select or clear a state error beside the diagram + const stateErrorButton = target.closest?.('.state-error-select'); + if (stateErrorButton) { + e.stopPropagation(); + const key = stateErrorButton.getAttribute('data-state-error-key'); + const error = getStateMachineErrors(diagnostics, diagnosticStateMachine ?? stateMachine) + .find(stateError => getStateErrorKey(stateError) === key); + const isSelected = !!diagnosticStateMachineError && getStateErrorKey(diagnosticStateMachineError) === key; + selectStateError(isSelected ? undefined : error); + if (key) focusStateError(root, key); + return; + } + if (target.closest?.('#state-error-clear-btn')) { + e.stopPropagation(); + const previousError = diagnosticStateMachineError; + selectStateError(undefined); + if (previousError) focusStateError(root, getStateErrorKey(previousError)); return; } @@ -273,6 +292,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (tab === 'fsm') { diagnosticStateMachine = undefined; diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; } selectedTab = tab; updateView(); @@ -342,16 +362,11 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) case 'diagnostics': { diagnostics = msg.diagnostics as LJDiagnostic[]; if (diagnosticStateMachine) { - const updatedError = diagnostics.find(diagnostic => - diagnostic.type === 'state-refinement-error' - && diagnostic.file.toLowerCase() === diagnosticStateMachineFile?.toLowerCase() - && diagnostic.stateMachine?.className === diagnosticStateMachine?.className - ); - diagnosticStateMachine = updatedError?.type === 'state-refinement-error' - ? updatedError.stateMachine ?? diagnosticStateMachine - : { ...diagnosticStateMachine, errorContext: null }; + const updatedError = findStateError(getStateMachineErrors(diagnostics, diagnosticStateMachine), diagnosticStateMachineError); + if (updatedError) selectStateError(updatedError, false); + else clearStateErrorSelection(); } - if (selectedTab === 'diagnostics' || (selectedTab === 'fsm' && diagnosticStateMachine)) updateView(); + if (selectedTab === 'diagnostics' || selectedTab === 'fsm') updateView(); break; } case 'file': @@ -359,6 +374,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView(); diagnosticStateMachine = undefined; diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; stateMachine = undefined; currentDiagram = ''; if (selectedTab === 'fsm') updateView(); @@ -404,7 +420,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const displayedStateMachine = diagnosticStateMachine ?? stateMachine; const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; - renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions); + const errorList = renderStateErrorList(getStateMachineErrors(diagnostics, displayedStateMachine), diagnosticStateMachineError); + renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, errorList); if (displayedStateMachine) renderMermaidDiagram(document, window); break; } @@ -414,6 +431,33 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } } + /** + * Shows a state error on its state machine, or the general diagram when no error is given + * @param error The state error to select + * @param render Whether to update the view + */ + function selectStateError(error: StateRefinementError | undefined, render = true) { + if (error?.stateMachine) { + diagnosticStateMachine = error.stateMachine; + diagnosticStateMachineFile = error.file; + diagnosticStateMachineError = error; + } else { + clearStateErrorSelection(); + } + currentDiagram = ''; + if (render) updateView(); + } + + function clearStateErrorSelection() { + if (diagnosticStateMachine) { + diagnosticStateMachine = stateMachine?.className === diagnosticStateMachine.className + ? undefined + : { ...diagnosticStateMachine, errorContext: null }; + } + diagnosticStateMachineFile = undefined; + diagnosticStateMachineError = undefined; + } + function revealDiagnostic(target: DiagnosticRevealTarget) { selectedTab = 'diagnostics'; diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index e26a633..f0dc172 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -1016,5 +1016,94 @@ export function getStyles(): string { fill: var(--vscode-errorForeground) !important; stroke: var(--vscode-errorForeground) !important; } + .fsm-layout { + display: flex; + flex-wrap: wrap; + align-items: flex-start; + gap: 1rem; + } + .fsm-layout .diagram-section { + flex: 3 1 24rem; + min-width: 0; + } + .state-errors { + flex: 1 1 14rem; + min-width: 0; + } + .state-errors-header { + display: flex; + align-items: baseline; + justify-content: space-between; + flex-wrap: wrap; + gap: 0.5rem; + margin-bottom: 0.5rem; + } + .state-errors-header h3 { + margin: 0; + font-size: 0.95rem; + } + .state-errors-count { + font-weight: normal; + opacity: 0.7; + } + .state-errors-header .underline-button { + margin-bottom: 0; + } + .state-errors-header .underline-button:disabled { + opacity: 0.35; + cursor: default; + } + .state-error-item { + background-color: var(--vscode-textCodeBlock-background); + border-radius: 4px; + margin-bottom: 0.5rem; + padding: 0.25rem 0.5rem 0.5rem; + outline: 1px solid transparent; + } + .state-error-item.selected { + outline: 2px solid var(--vscode-focusBorder); + } + .state-error-select { + display: flex; + align-items: flex-start; + gap: 0.5rem; + width: 100%; + padding: 0.25rem 0; + color: var(--vscode-foreground); + background: none; + border: none; + text-align: left; + } + .state-error-select:hover { + background: none; + } + .state-error-select:focus-visible { + outline: 1px solid var(--vscode-focusBorder); + outline-offset: 0; + } + .state-error-marker { + flex-shrink: 0; + margin-top: 0.2rem; + } + .state-error-item.selected .state-error-marker { + color: var(--vscode-focusBorder); + } + .state-error-details { + display: flex; + flex-direction: column; + gap: 0.15rem; + min-width: 0; + overflow-wrap: anywhere; + } + .state-error-call { + font-weight: 600; + } + .state-error-label { + opacity: 0.8; + } + .state-error-location { + padding-left: 1.5rem; + font-size: 0.85rem; + } `; } diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 263090d..79643f6 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -3,13 +3,13 @@ import { renderCodiconButton } from "../../icons"; import { escapeHtml } from "../../utils"; import { renderMainHeader } from "../sections"; -export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean) { +export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, errorList = '') { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; const diagramHeight = previousDiagramContainer?.offsetHeight; - root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight); + root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, diagramHeight, errorList); } -function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number): string { +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, diagramHeight?: number, errorList = ''): string { const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.toCondition) || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition) @@ -22,6 +22,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
${renderMainHeader("", 'fsm')} ${sm ? /*html*/` + ${errorList ? '
' : ''}
@@ -45,7 +46,8 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str 
${diagram}
-
` +
+ ${errorList ? `${errorList}
` : ''}` : 'No state machine available for the current file'} `; diff --git a/client/src/webview/views/fsm/state-errors.spec.ts b/client/src/webview/views/fsm/state-errors.spec.ts new file mode 100644 index 0000000..bd2a713 --- /dev/null +++ b/client/src/webview/views/fsm/state-errors.spec.ts @@ -0,0 +1,144 @@ +import { afterEach, describe, expect, it } from 'vitest'; +import type { LJDiagnostic, StateRefinementError } from '../../../types/diagnostics'; +import type { LJStateMachine, LJStateMachineErrorContext } from '../../../types/fsm'; +import { findStateError, getStateErrorKey, getStateErrorSummary, getStateMachineErrors, renderStateErrorList } from './state-errors'; +import { renderStateMachineView } from './fsm'; + +const refinementsFile = '/workspace/src/DefaultMutableTreeNodeRefinements.java'; +const callerFile = '/workspace/src/OutlineBuilder.java'; + +function machine(errorContext: LJStateMachineErrorContext | null = null, className = 'javax.swing.tree.DefaultMutableTreeNode'): LJStateMachine { + return { + className, states: ['childrenAllowed', 'maybeHasChildren'], + initialTransitions: [{ to: 'childrenAllowed' }], + transitions: [{ from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }], + errorContext, + }; +} + +function stateError(line: number, overrides: Partial = {}): StateRefinementError { + return { + category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', + message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hint: null, + file: callerFile, position: { file: callerFile, lineStart: line, colStart: 15, lineEnd: line, colEnd: 35 }, + translationTable: {}, expected: 'maybeHasChildren(root¹⁸)', + found: { implication: { name: 'root¹⁸', type: 'DefaultMutableTreeNode', predicate: 'childrenAllowed(root¹⁸)', next: null }, origin: null, simplification: null }, + customMessage: '', + declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }, + stateMachine: machine({ calledMethod: null, actualStates: ['childrenAllowed'] }), + ...overrides, + }; +} + +const fullContext: LJStateMachineErrorContext = { + calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'], receiver: 'root', + expectedStates: ['maybeHasChildren'], expectedCondition: 'maybeHasChildren(root)', + foundCondition: 'childrenAllowed(root)', definiteFoundState: 'childrenAllowed', +}; + +afterEach(() => { + document.body.innerHTML = ''; +}); + +describe('state machine errors', () => { + it('matches errors to the machine by class, not by file', () => { + const matching = stateError(10); + const otherClass = stateError(12, { stateMachine: machine(null, 'java.util.ArrayList') }); + const withoutMachine = stateError(14, { stateMachine: null }); + const refinementError = { ...stateError(16), type: 'custom-error' } as unknown as LJDiagnostic; + + expect(getStateMachineErrors([matching, otherClass, withoutMachine, refinementError], machine())).toEqual([matching]); + expect(getStateMachineErrors([matching], undefined)).toEqual([]); + expect(getStateMachineErrors(undefined, machine())).toEqual([]); + }); + + it('summarizes errors with the state machine error context', () => { + expect(getStateErrorSummary(stateError(10, { stateMachine: machine(fullContext) }))).toEqual({ + call: 'root.getFirstChild()', receiver: 'root', found: 'childrenAllowed', required: 'maybeHasChildren', + }); + expect(getStateErrorSummary(stateError(10, { stateMachine: machine({ + calledMethod: 'getFirstChild', actualStates: [], expectedStates: [], + expectedCondition: 'maybeHasChildren(root)', foundCondition: 'true', definiteFoundState: null, + }) }))).toEqual({ + call: 'getFirstChild()', receiver: null, found: 'true', required: 'maybeHasChildren(root)', + }); + }); + + it('falls back to the diagnostic text without the extended error context', () => { + expect(getStateErrorSummary(stateError(10))).toEqual({ + call: null, receiver: null, found: 'childrenAllowed(root¹⁸)', required: 'maybeHasChildren(root¹⁸)', + }); + + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([stateError(10)], undefined)); + const item = document.querySelector('.state-error-item')!; + expect(item.querySelector('.state-error-call')?.textContent).toBe('State Refinement Error'); + expect(item.textContent).not.toContain('Receiver:'); + expect(item.textContent).toContain('Found: childrenAllowed(root¹⁸)'); + expect(item.textContent).toContain('Required: maybeHasChildren(root¹⁸)'); + }); + + it('renders each error with its call, receiver, states, and source link beside the diagram', () => { + const errors = [stateError(10, { stateMachine: machine(fullContext) }), stateError(15)]; + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList(errors, undefined)); + + const layout = document.querySelector('.fsm-layout')!; + expect(Array.from(layout.children, child => child.className)).toEqual(['diagram-section', 'state-errors']); + expect(document.querySelector('#state-errors-title')?.textContent).toBe('State Errors (2)'); + const [first, second] = Array.from(document.querySelectorAll('.state-error-item')); + const details = Array.from(first.querySelectorAll('.state-error-details > *'), node => node.textContent?.replace(/\s+/g, ' ').trim()); + expect(details).toEqual(['root.getFirstChild()', 'Receiver: root', 'Found: childrenAllowed', 'Required: maybeHasChildren']); + const link = first.querySelector('.state-error-location .location-link')!; + expect(link.textContent).toBe('OutlineBuilder.java:11'); + expect(link.getAttribute('data-file')).toBe(callerFile); + expect(link.getAttribute('data-line')).toBe('10'); + expect(link.closest('button')).toBeNull(); + expect(second.querySelector('.location-link')?.textContent).toBe('OutlineBuilder.java:16'); + expect(document.querySelector('#state-error-clear-btn')?.disabled).toBe(true); + }); + + it('marks the selected error with state, icon, and enabled clear button', () => { + const errors = [stateError(10), stateError(15)]; + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList(errors, errors[1])); + + const buttons = Array.from(document.querySelectorAll('.state-error-select')); + expect(buttons.map(button => button.getAttribute('aria-pressed'))).toEqual(['false', 'true']); + expect(buttons.map(button => button.tagName)).toEqual(['BUTTON', 'BUTTON']); + expect(buttons[0].querySelector('.codicon-circle-large-outline')).not.toBeNull(); + expect(buttons[1].querySelector('.codicon-pass-filled')).not.toBeNull(); + expect(buttons[1].closest('.state-error-item')?.classList.contains('selected')).toBe(true); + expect(buttons[1].getAttribute('data-state-error-key')).toBe(getStateErrorKey(errors[1])); + expect(document.querySelector('#state-error-clear-btn')?.disabled).toBe(false); + }); + + it('leaves the view unchanged when there are no state errors', () => { + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false); + const withoutList = document.body.innerHTML; + + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([], undefined)); + + expect(renderStateErrorList([], undefined)).toBe(''); + expect(document.body.innerHTML).toBe(withoutList); + expect(document.querySelector('.fsm-layout')).toBeNull(); + expect(document.querySelector('.state-errors')).toBeNull(); + }); + + it('escapes error text', () => { + const error = stateError(10, { stateMachine: machine({ ...fullContext, receiver: '', calledMethod: 'run' }) }); + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([error], undefined)); + + expect(document.querySelector('.state-error-call')?.textContent).toBe('.run()'); + expect(document.querySelector('.state-errors img')).toBeNull(); + }); + + it('finds the selected error again after verification', () => { + const selected = stateError(10); + const moved = stateError(12); + const otherCall = stateError(20, { declarationPosition: { file: refinementsFile, lineStart: 18, colStart: 29, lineEnd: 18, colEnd: 51 } }); + + expect(findStateError([otherCall, stateError(10)], selected)).toEqual(selected); + expect(findStateError([otherCall, moved], selected)).toBe(moved); + expect(findStateError([otherCall], selected)).toBeUndefined(); + expect(findStateError([moved, stateError(14)], selected)).toBeUndefined(); + expect(findStateError([selected], undefined)).toBeUndefined(); + }); +}); diff --git a/client/src/webview/views/fsm/state-errors.ts b/client/src/webview/views/fsm/state-errors.ts new file mode 100644 index 0000000..2bfdd0a --- /dev/null +++ b/client/src/webview/views/fsm/state-errors.ts @@ -0,0 +1,156 @@ +import type { LJDiagnostic, StateRefinementError } from "../../../types/diagnostics"; +import type { LJStateMachine } from "../../../types/fsm"; +import type { VCImplication } from "../../../types/vc-implications"; +import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../../diagnostic-reveal"; +import { renderHighlightedInlineExpression } from "../../highlighting"; +import { renderCodicon } from "../../icons"; +import { escapeHtml } from "../../utils"; +import { renderLocationLink } from "../sections"; + +export type StateErrorSummary = { + call: string | null; + receiver: string | null; + found: string; + required: string; +}; + +/** + * Returns the state refinement errors that belong to the given state machine + * @param diagnostics All diagnostics in the workspace + * @param sm The displayed state machine + */ +export function getStateMachineErrors(diagnostics: LJDiagnostic[] | undefined, sm: LJStateMachine | undefined): StateRefinementError[] { + if (!diagnostics || !sm) return []; + return diagnostics.filter((diagnostic): diagnostic is StateRefinementError => + diagnostic.type === 'state-refinement-error' && belongsToStateMachine(diagnostic, sm) + ); +} + +// errors are usually reported in the caller file, so they are matched by class instead of file +function belongsToStateMachine(error: StateRefinementError, sm: LJStateMachine): boolean { + return !!error.stateMachine && error.stateMachine.className === sm.className; +} + +export function getStateErrorKey(error: StateRefinementError): string { + const target = getDiagnosticRevealTarget(error); + return target ? getDiagnosticRevealTargetKey(target) : `${error.file}:${error.message}`; +} + +/** + * Finds the selected error again after a new verification + * Falls back to the only error in the same file for the same called method, since edits can move the error position + * @param errors The errors of the displayed state machine + * @param selected The previously selected error + */ +export function findStateError(errors: StateRefinementError[], selected: StateRefinementError | undefined): StateRefinementError | undefined { + if (!selected) return undefined; + const key = getStateErrorKey(selected); + const exact = errors.find(error => getStateErrorKey(error) === key); + const declarationKey = getDeclarationKey(selected); + if (exact || !declarationKey) return exact; + + const candidates = errors.filter(error => + error.file.toLowerCase() === selected.file.toLowerCase() && getDeclarationKey(error) === declarationKey + ); + return candidates.length === 1 ? candidates[0] : undefined; +} + +function getDeclarationKey(error: StateRefinementError): string | undefined { + const position = error.declarationPosition; + if (!position?.file) return undefined; + return getDiagnosticRevealTargetKey({ file: position.file, position }); +} + +/** + * Summarizes an error with the state machine error context, falling back to the diagnostic text + * @param error The state refinement error + */ +export function getStateErrorSummary(error: StateRefinementError): StateErrorSummary { + const context = error.stateMachine?.errorContext; + const receiver = context?.receiver || null; + const calledMethod = context?.calledMethod || null; + const call = calledMethod ? `${receiver ? `${receiver}.` : ''}${calledMethod}()` : null; + const found = context?.definiteFoundState || context?.foundCondition || formatFound(error.found?.implication); + const required = context?.expectedStates?.length + ? context.expectedStates.join(' || ') + : context?.expectedCondition || error.expected || ''; + return { call, receiver, found, required }; +} + +function formatFound(implication: VCImplication | null | undefined): string { + const predicates: string[] = []; + for (let node = implication; node; node = node.next) { + if (node.predicate) predicates.push(node.predicate); + } + return predicates.join(' && '); +} + +/** + * Renders the list of state errors shown beside the diagram + * @param errors The errors of the displayed state machine + * @param selected The selected error, if any + * @returns The list HTML, or an empty string when there are no errors + */ +export function renderStateErrorList(errors: StateRefinementError[], selected: StateRefinementError | undefined): string { + if (errors.length === 0) return ''; + const selectedKey = selected ? getStateErrorKey(selected) : undefined; + const hasSelection = errors.some(error => getStateErrorKey(error) === selectedKey); + + return /*html*/` +
+
+

State Errors (${errors.length})

+ +
+
    + ${errors.map(error => renderStateErrorItem(error, getStateErrorKey(error) === selectedKey)).join('')} +
+
+ `; +} + +function renderStateErrorItem(error: StateRefinementError, selected: boolean): string { + const summary = getStateErrorSummary(error); + const key = getStateErrorKey(error); + const position = error.position ? { ...error.position, file: error.position.file || error.file } : undefined; + + return /*html*/` +
  • + + ${position ? `
    ${renderLocationLink(position)}
    ` : ''} +
    • + `; +} + +function renderDetail(label: string, value: string): string { + return /*html*/`${label}: ${value}`; +} + +function renderExpression(expression: string): string { + return `${renderHighlightedInlineExpression(expression)}`; +} + +/** + * Restores keyboard focus on an error after the view is rendered again + * @param root The webview root element + * @param key The key of the error to focus + */ +export function focusStateError(root: HTMLElement, key: string) { + const button = Array.from(root.querySelectorAll('.state-error-select')) + .find(element => element.getAttribute('data-state-error-key') === key); + button?.focus(); +} diff --git a/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java b/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java new file mode 100644 index 0000000..d2f09a3 --- /dev/null +++ b/client/test-fixtures/failing/src/main/java/FailingTreeNodeState.java @@ -0,0 +1,11 @@ +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.TreeNode; + +public class FailingTreeNodeState { + TreeNode rebuild() { + DefaultMutableTreeNode root = new DefaultMutableTreeNode("root"); + root.add(new DefaultMutableTreeNode("first")); + root.removeAllChildren(); + return root.getFirstChild(); + } +} diff --git a/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java b/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java new file mode 100644 index 0000000..47c1d7a --- /dev/null +++ b/client/test-fixtures/failing/src/main/java/TreeNodeRefinements.java @@ -0,0 +1,22 @@ +import javax.swing.tree.MutableTreeNode; +import javax.swing.tree.TreeNode; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.tree.DefaultMutableTreeNode") +@StateSet({"childrenAllowed", "maybeHasChildren"}) +public interface TreeNodeRefinements { + @StateRefinement(to = "childrenAllowed(this)") + void DefaultMutableTreeNode(Object userObject); + + @StateRefinement(from = "childrenAllowed(this)", to = "maybeHasChildren(this)") + void add(MutableTreeNode newChild); + + @StateRefinement(from = "maybeHasChildren(this)", to = "childrenAllowed(this)") + void removeAllChildren(); + + @StateRefinement(from = "maybeHasChildren(this)") + TreeNode getFirstChild(); +} From 64b4b6e5cd81fe5cc99fae2c89fcffc9bde6ae9a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 20 Oct 2026 23:53:14 +0100 Subject: [PATCH 2/4] Pad selected state errors so the source link clears the outline Co-Authored-By: Claude Opus 5.5 --- client/src/webview/styles.ts | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index f0dc172..66d0a25 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -1057,18 +1057,18 @@ export function getStyles(): string { background-color: var(--vscode-textCodeBlock-background); border-radius: 4px; margin-bottom: 0.5rem; - padding: 0.25rem 0.5rem 0.5rem; - outline: 1px solid transparent; + padding: 0.5rem; + outline: 2px solid transparent; } .state-error-item.selected { - outline: 2px solid var(--vscode-focusBorder); + outline-color: var(--vscode-focusBorder); } .state-error-select { display: flex; align-items: flex-start; gap: 0.5rem; width: 100%; - padding: 0.25rem 0; + padding: 0.25rem; color: var(--vscode-foreground); background: none; border: none; @@ -1079,7 +1079,7 @@ export function getStyles(): string { } .state-error-select:focus-visible { outline: 1px solid var(--vscode-focusBorder); - outline-offset: 0; + outline-offset: -1px; } .state-error-marker { flex-shrink: 0; @@ -1102,7 +1102,8 @@ export function getStyles(): string { opacity: 0.8; } .state-error-location { - padding-left: 1.5rem; + margin-top: 0.25rem; + padding: 0 0.25rem 0.25rem 1.75rem; font-size: 0.85rem; } `; From bf91c18a16137924c80f3d90b263ae0e08e1b2ba Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 21 Oct 2026 00:00:18 +0100 Subject: [PATCH 3/4] Address review of the state error list - Keep a selection after verification only when its error still exists; the moved-position fallback now needs a single matching call both before and after, so a fixed error never hands its selection to a sibling for the same method. - Refresh the general diagram from the latest error machines after the selection is cleared or fixed, instead of keeping a stale copy. - Skip re-rendering the State Machine view when neither the diagram nor the list changed, and restore focus to the same error after rendering. - Make position-less error keys distinct, escape source link files, and build the diagram and list layout in one expression. - Make the integration test fail on timeouts and assert on the messages sent to the webview. Co-Authored-By: Claude Opus 5.5 --- client/src/test/state-errors.test.ts | 51 ++++++++++------ client/src/webview/script.spec.ts | 61 +++++++++++++++++++ client/src/webview/script.ts | 30 +++++++-- client/src/webview/views/fsm/fsm.ts | 10 +-- .../webview/views/fsm/state-errors.spec.ts | 36 +++++++++-- client/src/webview/views/fsm/state-errors.ts | 19 +++--- client/src/webview/views/sections.ts | 2 +- 7 files changed, 168 insertions(+), 41 deletions(-) diff --git a/client/src/test/state-errors.test.ts b/client/src/test/state-errors.test.ts index c6aff26..37d7c82 100644 --- a/client/src/test/state-errors.test.ts +++ b/client/src/test/state-errors.test.ts @@ -3,10 +3,10 @@ import * as path from 'node:path'; import * as vscode from 'vscode'; import type { LJDiagnostic, StateRefinementError } from '../types/diagnostics'; import type { LJStateMachine } from '../types/fsm'; -import type { LiquidJavaTestApi } from '../types/test-api'; +import type { LiquidJavaTestApi, WebviewMessage } from '../types/test-api'; suite('Bundled LiquidJava state machine errors', () => { - test('sends state errors from the caller file with the machine of the refinements file', async () => { + test('sends the webview state errors from the caller file with the machine of the refinements file', async () => { const installed = vscode.extensions.getExtension('AlcidesFonseca.liquid-java'); assert.ok(installed); const api = await installed.activate(); @@ -17,33 +17,46 @@ suite('Bundled LiquidJava state machine errors', () => { const refinementsUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/TreeNodeRefinements.java'); const callerUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/FailingTreeNodeState.java'); const sameFile = (file: string, uri: vscode.Uri) => vscode.Uri.file(path.resolve(file)).fsPath === uri.fsPath; - const subscriptions: vscode.Disposable[] = []; const isStateError = (diagnostic: LJDiagnostic): diagnostic is StateRefinementError => diagnostic.type === 'state-refinement-error' && sameFile(diagnostic.file, callerUri); + const subscriptions: vscode.Disposable[] = []; + const nextWebviewMessage = (description: string, matches: (event: WebviewMessage) => T | undefined) => + new Promise((resolve, reject) => { + const timeout = setTimeout(() => reject(new Error(`Timed out waiting for ${description}`)), 90_000); + const done = (callback: () => void) => { + clearTimeout(timeout); + subscription.dispose(); + failure.dispose(); + callback(); + }; + const subscription = api.onWebviewMessage(event => { + const value = matches(event); + if (value !== undefined) done(() => resolve(value)); + }); + const failure = api.onFailure(() => + done(() => reject(new Error(`LiquidJava verifier crashed while waiting for ${description}`)))); + subscriptions.push(subscription, failure, { dispose: () => clearTimeout(timeout) }); + }); try { - const ready = new Promise(resolve => subscriptions.push(api.onWebviewMessage(event => { - if (event.direction === 'fromWebview' && event.message.type === 'ready') resolve(); - }))); + // hide the view first so showing it always loads a fresh webview + await vscode.commands.executeCommand('workbench.action.closeSidebar'); + const ready = nextWebviewMessage('the webview to be ready', event => + event.direction === 'fromWebview' && event.message.type === 'ready' ? true : undefined); await vscode.commands.executeCommand('liquidjava.showView'); - await Promise.race([ready, new Promise(resolve => setTimeout(resolve, 5000))]); + await ready; - const machine = new Promise(resolve => subscriptions.push(api.onWebviewMessage(event => { - if (event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm) resolve(event.message.sm); - }))); - const diagnostics = new Promise((resolve, reject) => { - subscriptions.push(api.onDiagnostics(value => { - if (value.some(isStateError)) resolve(value); - })); - subscriptions.push(api.onFailure(() => reject(new Error('LiquidJava verifier crashed while checking state errors')))); - }); + const machine = nextWebviewMessage('the refinements file state machine', event => + event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm + ? event.message.sm as LJStateMachine : undefined); + const stateError = nextWebviewMessage('the state error diagnostics', event => + event.direction === 'toWebview' && event.message.type === 'diagnostics' + ? (event.message.diagnostics as LJDiagnostic[]).find(isStateError) : undefined); const document = await vscode.workspace.openTextDocument(refinementsUri); await vscode.window.showTextDocument(document); await vscode.commands.executeCommand('liquidjava.verify'); - const [sm, result] = await Promise.all([machine, diagnostics]); - const error = result.find(isStateError); - assert.ok(error, JSON.stringify(result)); + const [sm, error] = await Promise.all([machine, stateError]); assert.equal(sm.className, 'javax.swing.tree.DefaultMutableTreeNode'); assert.ok(error.stateMachine, 'the state error must carry its state machine'); assert.equal(error.stateMachine.className, sm.className, 'errors are matched to the machine by class'); diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index b7d4053..34edc0e 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -358,6 +358,67 @@ describe('webview script', () => { expect(mermaidSource()).not.toContain('lj-state-error-method'); }); + it('drops a fixed selection instead of selecting a sibling error for the same call', () => { + const sibling = stateError(20, 'getFirstChild', 'node'); + showStateMachine([firstChildError, sibling]); + items()[0].click(); + + receive({ type: 'diagnostics', diagnostics: [stateError(20, 'getFirstChild', 'node')] }); + expect(calls()).toEqual(['node.getFirstChild()']); + expect(pressed()).toEqual(['false']); + expect(mermaidSource()).not.toContain('lj-state-error-method'); + }); + + it('refreshes a machine from another file after its selection is cleared or fixed', () => { + // edits to the refinements file add a method to every error machine + const withState = (error: StateRefinementError, method: string): StateRefinementError => ({ + ...error, + stateMachine: { ...error.stateMachine!, transitions: [ + ...treeMachine.transitions, { from: 'childrenAllowed', to: 'childrenAllowed', label: method }, + ] }, + }); + // the caller file has no machine, so the diagram comes from the errors + receive({ type: 'file', file: otherFile }); + receive({ type: 'diagnostics', diagnostics: [firstChildError, removeError] }); + receive({ type: 'status', status: 'failed' }); + receive({ type: 'fsm', sm: null }); + root.querySelectorAll('.diagnostic-state-machine-btn')[0].click(); + click('#state-error-clear-btn'); + + receive({ type: 'diagnostics', diagnostics: [withState(firstChildError, 'cleared'), withState(removeError, 'cleared')] }); + expect(root.querySelector('.state-errors')).not.toBeNull(); + expect(root.querySelector('.mermaid')?.textContent).toContain('cleared'); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + + items()[0].click(); + receive({ type: 'diagnostics', diagnostics: [withState(removeError, 'fixed')] }); + expect(calls()).toEqual(['menu.removeAllChildren()']); + expect(pressed()).toEqual(['false']); + expect(root.querySelector('.mermaid')?.textContent).toContain('fixed'); + expect(mermaidSource()).not.toContain('ljStateErrorActual'); + }); + + it('keeps the rendered view and focus when a verification changes nothing', () => { + showStateMachine([firstChildError, removeError]); + items()[1].click(); + const renderedItem = items()[1]; + const mermaidRuns = runMermaid.mock.calls.length; + expect(dom.window.document.activeElement).toBe(renderedItem); + + receive({ type: 'diagnostics', diagnostics: [stateError(10, 'getFirstChild', 'root'), stateError(15, 'removeAllChildren', 'menu')] }); + receive({ type: 'status', status: 'failed' }); + expect(items()[1]).toBe(renderedItem); + expect(runMermaid.mock.calls.length).toBe(mermaidRuns); + expect(dom.window.document.activeElement).toBe(renderedItem); + + // a changed list is rendered again with focus on the same error + receive({ type: 'diagnostics', diagnostics: [stateError(15, 'removeAllChildren', 'menu'), stateError(30, 'getFirstChild', 'node')] }); + expect(calls()).toEqual(['menu.removeAllChildren()', 'node.getFirstChild()']); + expect(runMermaid.mock.calls.length).toBe(mermaidRuns + 1); + expect(dom.window.document.activeElement).toBe(items()[0]); + expect(pressed()).toEqual(['true', 'false']); + }); + it('leaves the view unchanged when the machine has no state errors', () => { showStateMachine([diagnostic(currentFile, 'Unrelated error')]); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 2052b69..357a461 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -35,6 +35,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let diagnosticStateMachine: LJStateMachine | undefined; let diagnosticStateMachineFile: string | undefined; let diagnosticStateMachineError: StateRefinementError | undefined; + let renderedStateMachineView: string | undefined; let context: LJContext; let errorAtCursor: RefinementMismatchError; let selectedTab: NavTab = 'diagnostics'; @@ -360,11 +361,14 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) updateView(); break; case 'diagnostics': { + const previousDiagnostics = diagnostics; diagnostics = msg.diagnostics as LJDiagnostic[]; if (diagnosticStateMachine) { - const updatedError = findStateError(getStateMachineErrors(diagnostics, diagnosticStateMachine), diagnosticStateMachineError); + const errors = getStateMachineErrors(diagnostics, diagnosticStateMachine); + const updatedError = findStateError(errors, diagnosticStateMachineError, + getStateMachineErrors(previousDiagnostics, diagnosticStateMachine)); if (updatedError) selectStateError(updatedError, false); - else clearStateErrorSelection(); + else clearStateErrorSelection(errors); } if (selectedTab === 'diagnostics' || selectedTab === 'fsm') updateView(); break; @@ -399,6 +403,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) * Updates the webview content based on the current state */ function updateView() { + const previousStateMachineView = renderedStateMachineView; + renderedStateMachineView = undefined; if (status === 'stopped' || status === 'crashed') { currentDiagram = ''; root.innerHTML = renderStopped(status); @@ -421,7 +427,13 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions); currentDiagram = diagram; const errorList = renderStateErrorList(getStateMachineErrors(diagnostics, displayedStateMachine), diagnosticStateMachineError); + // skip unchanged views, since every verification would otherwise redraw the diagram + renderedStateMachineView = `${diagram}\n${errorList}`; + if (renderedStateMachineView === previousStateMachineView) break; + + const focusedStateError = document.activeElement?.closest?.('.state-error-select')?.getAttribute('data-state-error-key'); renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, errorList); + if (focusedStateError) focusStateError(root, focusedStateError); if (displayedStateMachine) renderMermaidDiagram(document, window); break; } @@ -442,17 +454,23 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) diagnosticStateMachineFile = error.file; diagnosticStateMachineError = error; } else { - clearStateErrorSelection(); + clearStateErrorSelection(getStateMachineErrors(diagnostics, diagnosticStateMachine)); } + if (!render) return; currentDiagram = ''; - if (render) updateView(); + updateView(); } - function clearStateErrorSelection() { + /** + * Shows the general diagram of the displayed state machine + * @param errors The current errors of the displayed state machine, used to refresh a machine from another file + */ + function clearStateErrorSelection(errors: StateRefinementError[]) { if (diagnosticStateMachine) { + const latestStateMachine = errors.find(error => error.stateMachine)?.stateMachine ?? diagnosticStateMachine; diagnosticStateMachine = stateMachine?.className === diagnosticStateMachine.className ? undefined - : { ...diagnosticStateMachine, errorContext: null }; + : { ...latestStateMachine, errorContext: null }; } diagnosticStateMachineFile = undefined; diagnosticStateMachineError = undefined; diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 79643f6..dc133ce 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -21,8 +21,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
    ${renderMainHeader("", 'fsm')} - ${sm ? /*html*/` - ${errorList ? '
    ' : ''} + ${sm ? renderWithErrorList(/*html*/`
    @@ -46,9 +45,12 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str 
    ${diagram}
    -
    - ${errorList ? `${errorList}
    ` : ''}` +
    `, errorList) : 'No state machine available for the current file'} `; } + +function renderWithErrorList(diagramSection: string, errorList: string): string { + return errorList ? /*html*/`
    ${diagramSection}${errorList}
    ` : diagramSection; +} diff --git a/client/src/webview/views/fsm/state-errors.spec.ts b/client/src/webview/views/fsm/state-errors.spec.ts index bd2a713..3a37b39 100644 --- a/client/src/webview/views/fsm/state-errors.spec.ts +++ b/client/src/webview/views/fsm/state-errors.spec.ts @@ -135,10 +135,38 @@ describe('state machine errors', () => { const moved = stateError(12); const otherCall = stateError(20, { declarationPosition: { file: refinementsFile, lineStart: 18, colStart: 29, lineEnd: 18, colEnd: 51 } }); - expect(findStateError([otherCall, stateError(10)], selected)).toEqual(selected); - expect(findStateError([otherCall, moved], selected)).toBe(moved); - expect(findStateError([otherCall], selected)).toBeUndefined(); - expect(findStateError([moved, stateError(14)], selected)).toBeUndefined(); + expect(findStateError([otherCall, stateError(10)], selected, [selected, otherCall])).toEqual(selected); + // an edit moved the only error of this call + expect(findStateError([otherCall, moved], selected, [selected, otherCall])).toBe(moved); + expect(findStateError([otherCall, moved], selected)).toBeUndefined(); + expect(findStateError([otherCall], selected, [selected, otherCall])).toBeUndefined(); + expect(findStateError([moved, stateError(14)], selected, [selected])).toBeUndefined(); expect(findStateError([selected], undefined)).toBeUndefined(); }); + + it('drops a fixed selection instead of moving it to a sibling for the same call', () => { + const selected = stateError(10); + const sibling = stateError(20); + + expect(findStateError([sibling], selected, [selected, sibling])).toBeUndefined(); + }); + + it('keeps keys distinct for errors without a position', () => { + const first = stateError(10, { position: null, title: 'State Refinement Error', message: 'a' }); + const second = stateError(10, { position: null, title: 'State Conflict', message: 'a' }); + + expect(getStateErrorKey(first)).not.toBe(getStateErrorKey(second)); + expect(getStateErrorKey(first)).not.toMatch(/:\d+:\d+-\d+:\d+$/); + expect(findStateError([second], first)).toBeUndefined(); + }); + + it('escapes the file of the source link', () => { + const file = '/workspace/src/"onmouseover="alert(1).java'; + const error = stateError(10, { file, position: { file, lineStart: 1, colStart: 0, lineEnd: 1, colEnd: 4 } }); + renderStateMachineView(document.body, machine(), 'diagram', 'TB', false, renderStateErrorList([error], undefined)); + + const link = document.querySelector('.state-error-location .location-link')!; + expect(link.getAttribute('data-file')).toBe(file); + expect(link.hasAttribute('onmouseover')).toBe(false); + }); }); diff --git a/client/src/webview/views/fsm/state-errors.ts b/client/src/webview/views/fsm/state-errors.ts index 2bfdd0a..9e0c5a0 100644 --- a/client/src/webview/views/fsm/state-errors.ts +++ b/client/src/webview/views/fsm/state-errors.ts @@ -33,26 +33,31 @@ function belongsToStateMachine(error: StateRefinementError, sm: LJStateMachine): export function getStateErrorKey(error: StateRefinementError): string { const target = getDiagnosticRevealTarget(error); - return target ? getDiagnosticRevealTargetKey(target) : `${error.file}:${error.message}`; + // errors without a position never match the position pattern of reveal keys + return target ? getDiagnosticRevealTargetKey(target) : `${error.file}#${error.title}#${error.message}`; } /** * Finds the selected error again after a new verification - * Falls back to the only error in the same file for the same called method, since edits can move the error position + * Since edits can move the error position, falls back to the same file and called method when that call was + * the only one before and after the verification, so a fixed error never passes its selection to a sibling * @param errors The errors of the displayed state machine * @param selected The previously selected error + * @param previousErrors The errors of the displayed state machine before the verification */ -export function findStateError(errors: StateRefinementError[], selected: StateRefinementError | undefined): StateRefinementError | undefined { +export function findStateError(errors: StateRefinementError[], selected: StateRefinementError | undefined, + previousErrors: StateRefinementError[] = []): StateRefinementError | undefined { if (!selected) return undefined; const key = getStateErrorKey(selected); const exact = errors.find(error => getStateErrorKey(error) === key); const declarationKey = getDeclarationKey(selected); if (exact || !declarationKey) return exact; - const candidates = errors.filter(error => - error.file.toLowerCase() === selected.file.toLowerCase() && getDeclarationKey(error) === declarationKey - ); - return candidates.length === 1 ? candidates[0] : undefined; + const isSameCall = (error: StateRefinementError) => + error.file.toLowerCase() === selected.file.toLowerCase() && getDeclarationKey(error) === declarationKey; + const candidates = errors.filter(isSameCall); + const previousCandidates = previousErrors.filter(isSameCall); + return candidates.length === 1 && previousCandidates.length === 1 ? candidates[0] : undefined; } function getDeclarationKey(error: StateRefinementError): string | undefined { diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index df94ec5..4502781 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -122,7 +122,7 @@ export function renderLocationLink(position?: SourcePosition): string { return /*html*/`${escapeHtml(getFile(position))}`; From 915088358705fef55b3b94289396d5a9003aa19a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 22 Oct 2026 00:02:48 +0100 Subject: [PATCH 4/4] Use liquidjava-fsm 0.1.4 for the failing call's error context Co-Authored-By: Claude Opus 5.5 --- server/pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/pom.xml b/server/pom.xml index 514d511..53bef18 100644 --- a/server/pom.xml +++ b/server/pom.xml @@ -172,7 +172,7 @@ io.github.liquid-java liquidjava-fsm - 0.1.3 + 0.1.4 tools.aqua