From 79accc2caeaf4d4e196d24674f292094aebdce67 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 24 Oct 2026 23:45:58 +0100 Subject: [PATCH 1/3] Keep the state error in the State Machine view and link it to the editor The tab keeps the last state error shown and follows the error at the cursor, steps through several errors, counts them on the tab, and links back to the error in the Verification tab. State errors get a labelled Show in state machine button and CodeLens. Co-Authored-By: Claude Opus 5.5 --- client/media/walkthrough/diagnostics.md | 2 +- client/media/walkthrough/state-machine.md | 2 +- client/package.json | 4 +- client/src/services/codelens.ts | 19 ++- client/src/services/webview.ts | 12 +- client/src/test/state-errors.test.ts | 88 ++++++++++ client/src/webview/script.spec.ts | 112 ++++++++++++- client/src/webview/script.ts | 152 +++++++++++++----- client/src/webview/state-errors.spec.ts | 92 +++++++++++ client/src/webview/state-errors.ts | 68 ++++++++ client/src/webview/styles.ts | 61 ++++++- client/src/webview/views/context/context.ts | 4 +- .../webview/views/diagnostics/diagnostics.ts | 3 +- .../src/webview/views/diagnostics/errors.ts | 2 +- client/src/webview/views/fsm/fsm.spec.ts | 46 ++++++ client/src/webview/views/fsm/fsm.ts | 61 +++++-- client/src/webview/views/sections.ts | 22 +-- .../src/main/java/FailingTreeNodeState.java | 11 ++ .../src/main/java/TreeNodeRefinements.java | 22 +++ 19 files changed, 694 insertions(+), 89 deletions(-) create mode 100644 client/src/test/state-errors.test.ts create mode 100644 client/src/webview/state-errors.spec.ts create mode 100644 client/src/webview/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/media/walkthrough/diagnostics.md b/client/media/walkthrough/diagnostics.md index 410e36a..eea2a6f 100644 --- a/client/media/walkthrough/diagnostics.md +++ b/client/media/walkthrough/diagnostics.md @@ -1,3 +1,3 @@ The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source. When a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available. -Switch between **Current file** and **Workspace**, or use **View related context** and **View error on state machine** to investigate an error. +Switch between **Current file** and **Workspace**, or use **View related context** and **Show in state machine** to investigate an error. diff --git a/client/media/walkthrough/state-machine.md b/client/media/walkthrough/state-machine.md index a12bc4b..a73bcfb 100644 --- a/client/media/walkthrough/state-machine.md +++ b/client/media/walkthrough/state-machine.md @@ -1,4 +1,4 @@ The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`. Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it. Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition. -From a state error, choose **View error on state machine** to see the related states and call. +From a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it. diff --git a/client/package.json b/client/package.json index 814ca37..cb02075 100644 --- a/client/package.json +++ b/client/package.json @@ -218,7 +218,7 @@ { "id": "diagnostics", "title": "Understand diagnostics", - "description": "The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source.\nWhen a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available.\nSwitch between **Current file** and **Workspace**, or use **View related context** and **View error on state machine** to investigate an error.\n[Open LiquidJava view](command:liquidjava.showView)", + "description": "The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source.\nWhen a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available.\nSwitch between **Current file** and **Workspace**, or use **View related context** and **Show in state machine** to investigate an error.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { "markdown": "media/walkthrough/diagnostics.md" }, @@ -240,7 +240,7 @@ { "id": "stateMachine", "title": "Explore state machines", - "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **View error on state machine** to see the related states and call.\n[Open LiquidJava view](command:liquidjava.showView)", + "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { "markdown": "media/walkthrough/state-machine.md" }, diff --git a/client/src/services/codelens.ts b/client/src/services/codelens.ts index 2a8c8c5..ca850c5 100644 --- a/client/src/services/codelens.ts +++ b/client/src/services/codelens.ts @@ -16,8 +16,7 @@ export function registerCodeLens(context: vscode.ExtensionContext) { const file = normalizeFilePath(document.uri.fsPath); return (extension.diagnostics || []) - .map(diagnostic => createDiagnosticCodeLens(diagnostic, file)) - .filter((codeLens): codeLens is vscode.CodeLens => Boolean(codeLens)); + .flatMap(diagnostic => createDiagnosticCodeLenses(diagnostic, file)); } }) ); @@ -27,18 +26,26 @@ export function refreshCodeLenses() { codeLensEmitter.fire(); } -function createDiagnosticCodeLens(diagnostic: LJDiagnostic, file: string): vscode.CodeLens | undefined { +function createDiagnosticCodeLenses(diagnostic: LJDiagnostic, file: string): vscode.CodeLens[] { const targetDiagnostic = getDiagnosticRevealTarget(diagnostic); - if (!targetDiagnostic || targetDiagnostic.file !== file) return undefined; + if (!targetDiagnostic || targetDiagnostic.file !== file) return []; const position = targetDiagnostic.position; const range = new vscode.Range( new vscode.Position(position.lineStart, position.colStart), new vscode.Position(position.lineStart, position.colStart) ); - return new vscode.CodeLens(range, { + const codeLenses = [new vscode.CodeLens(range, { title: diagnostic.title, command: "liquidjava.showView", arguments: [targetDiagnostic] - }); + })]; + if (diagnostic.type === 'state-refinement-error' && diagnostic.stateMachine) { + codeLenses.push(new vscode.CodeLens(range, { + title: "Show in state machine", + command: "liquidjava.showView", + arguments: [targetDiagnostic, 'fsm'] + })); + } + return codeLenses; } diff --git a/client/src/services/webview.ts b/client/src/services/webview.ts index c342595..1267214 100644 --- a/client/src/services/webview.ts +++ b/client/src/services/webview.ts @@ -2,6 +2,7 @@ import * as vscode from "vscode"; import { LiquidJavaWebviewProvider } from "../webview/provider"; import { extension } from "../state"; import type { DiagnosticRevealTarget } from "../types/diagnostics"; +import type { NavTab } from "../webview/views/sections"; /** * Initializes the webview panel for the extension @@ -9,7 +10,7 @@ import type { DiagnosticRevealTarget } from "../types/diagnostics"; */ export function registerWebview(context: vscode.ExtensionContext) { extension.webview = new LiquidJavaWebviewProvider(context.extensionUri); - let pendingDiagnosticReveal: DiagnosticRevealTarget | undefined; + let pendingDiagnosticReveal: { diagnostic: DiagnosticRevealTarget, tab?: NavTab } | undefined; // webview provider context.subscriptions.push( @@ -18,15 +19,16 @@ export function registerWebview(context: vscode.ExtensionContext) { ); // show view command context.subscriptions.push( - vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget) => { + // shows the diagnostic in the Verification tab, or a state error in the State Machine tab when tab is 'fsm' + vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget, tab?: NavTab) => { const isVisible = extension.webview?.isVisible(); await vscode.commands.executeCommand("liquidJavaView.focus"); if (!diagnostic) return; if (isVisible) { - extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic }); + extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic, tab }); } else { - pendingDiagnosticReveal = diagnostic; + pendingDiagnosticReveal = { diagnostic, tab }; } }) ); @@ -40,7 +42,7 @@ export function registerWebview(context: vscode.ExtensionContext) { if (extension.stateMachine !== undefined) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine }); if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status }); if (pendingDiagnosticReveal) { - extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic: pendingDiagnosticReveal }); + extension.webview?.sendMessage({ type: "revealDiagnostic", ...pendingDiagnosticReveal }); pendingDiagnosticReveal = undefined; } } diff --git a/client/src/test/state-errors.test.ts b/client/src/test/state-errors.test.ts new file mode 100644 index 0000000..0ceec2d --- /dev/null +++ b/client/src/test/state-errors.test.ts @@ -0,0 +1,88 @@ +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, WebviewMessage } from '../types/test-api'; + +suite('Bundled LiquidJava state machine errors', () => { + test('sends the webview state errors with their machine and shows them on it from the editor', 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 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 { + // 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 ready; + + 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, 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'); + 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)); + + // the editor offers to show the state error on its state machine + await vscode.window.showTextDocument(await vscode.workspace.openTextDocument(callerUri)); + const codeLenses = await vscode.commands.executeCommand('vscode.executeCodeLensProvider', callerUri); + const stateMachineLens = codeLenses.find(codeLens => codeLens.command?.title === 'Show in state machine'); + assert.ok(stateMachineLens?.command, 'state errors must have a CodeLens to show them on the state machine'); + assert.equal(stateMachineLens.command.command, 'liquidjava.showView'); + const [target, tab] = stateMachineLens.command.arguments ?? []; + assert.equal(tab, 'fsm'); + assert.deepEqual(target.position, error.position); + + const reveal = nextWebviewMessage('the state error to be shown on the state machine', event => + event.direction === 'toWebview' && event.message.type === 'revealDiagnostic' ? event.message : undefined); + await vscode.commands.executeCommand(stateMachineLens.command.command, ...stateMachineLens.command.arguments!); + const message = await reveal; + assert.equal(message.tab, 'fsm'); + assert.deepEqual((message.diagnostic as { position: unknown }).position, error.position); + } finally { + subscriptions.forEach(subscription => subscription.dispose()); + await vscode.commands.executeCommand('workbench.action.closeAllEditors'); + } + }); +}); diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index bed56cc..a45c230 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -186,12 +186,12 @@ describe('webview script', () => { expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed'); expect(Array.from(root.querySelectorAll('.mermaid .lj-dimmed-method'), node => node.textContent)).toEqual(['close()', 'reopen()']); - // the general diagram of the file has no error to focus on + // the tab keeps the error after visiting another tab click('[data-tab="diagnostics"]'); receive({ type: 'fsm', sm: stateMachine }); click('[data-tab="fsm"]'); - expect(root.querySelector('#diagram-focus-btn')).toBeNull(); - expect(root.querySelector('.mermaid')?.textContent).not.toContain('ljState'); + expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all'); + expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed'); }); it('keeps the zoom when toggling the dimming and resets it for a new error', async () => { @@ -264,6 +264,112 @@ describe('webview script', () => { expect(mouseDown('#diagram-wrapper')).toBe(true); }); + it('steps through the state errors of the file in source order', () => { + showDiagnostics([ + stateError('Second state error', errorMachine('Second', 'reset'), 9), + stateError('First state error', errorMachine('First', 'close'), 4), + ]); + expect(root.querySelector('[data-tab="fsm"] .nav-badge')?.textContent).toBe('2'); + + click('.diagnostic-state-machine-btn[data-error-index="1"]'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); + expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2'); + + click('.state-error-step-btn[data-step="1"]'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Second'); + expect(root.querySelector('.state-error-position')?.textContent).toBe('2 of 2'); + expect(root.querySelector('.diagram-error-text')?.textContent).toContain('counter.reset()'); + expect(root.querySelector('.state-error-step-btn[data-step="1"]')?.disabled).toBe(true); + + click('.state-error-step-btn[data-step="-1"]'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); + }); + + it('points to the state errors of the file until one is shown', () => { + showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]); + receive({ type: 'fsm', sm: stateMachine }); + click('[data-tab="fsm"]'); + expect(root.querySelector('.diagram-error-text')?.textContent).toBe('1 state error found'); + expect(root.querySelector('.mermaid')?.textContent).not.toContain('ljState'); + + click('#state-error-show-btn'); + expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all'); + expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed'); + }); + + it('follows the state error at the cursor without overriding a later choice', () => { + const first = stateError('First state error', errorMachine('First', 'close'), 4); + const second = stateError('Second state error', errorMachine('Second', 'reset'), 9); + showDiagnostics([first, second]); + + // the error reached by the cursor is shown when the tab opens + receive({ type: 'context', context: context(), errorAtCursor: second }); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics'); + click('[data-tab="fsm"]'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Second'); + + receive({ type: 'context', context: context(), errorAtCursor: first }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); + + // the same error at the cursor after a new verification keeps the error chosen in the view + click('.state-error-step-btn[data-step="1"]'); + receive({ type: 'context', context: context(), errorAtCursor: { ...first } }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Second'); + + // moving away and back to an error shows it again + receive({ type: 'context', context: context(), errorAtCursor: undefined }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Second'); + receive({ type: 'context', context: context(), errorAtCursor: first }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); + }); + + it('goes back to the shown state error in the Verification tab', () => { + // the other error is at another position, so only the state error is revealed + const error = stateError('State refinement error', errorMachine('Counter', 'close'), 7); + showDiagnostics([diagnostic(currentFile, 'Other error'), error]); + click('.diagnostic-state-machine-btn'); + + click('#state-error-reveal-btn'); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics'); + expect(root.querySelector('.diagnostic-item.revealed h3')?.textContent).toBe('State refinement error'); + }); + + it('opens a state error on the state machine from the editor', () => { + const error = stateError('State refinement error', errorMachine('Counter', 'close'), 7); + showDiagnostics([error]); + + receive({ type: 'revealDiagnostic', diagnostic: { file: currentFile, position: error.position }, tab: 'fsm' }); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('fsm'); + expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all'); + + // other diagnostics are still revealed in the Verification tab + receive({ type: 'revealDiagnostic', diagnostic: { file: currentFile, position: { ...position, lineStart: 1 } }, tab: 'fsm' }); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics'); + }); + + it('keeps the rendered diagram when a new verification does not change it', async () => { + const error = stateError('State refinement error', errorMachine('Counter', 'close')); + showDiagnostics([error]); + click('.diagnostic-state-machine-btn'); + const rendered = root.querySelector('.diagram-container'); + + receive({ type: 'diagnostics', diagnostics: [{ ...error }] }); + expect(root.querySelector('.diagram-container')).toBe(rendered); + expect(runMermaid).toHaveBeenCalledOnce(); + + // fixing the error clears it from the view + receive({ type: 'diagnostics', diagnostics: [] }); + expect(root.querySelector('#diagram-focus-btn')).toBeNull(); + expect(root.querySelector('.nav-badge')).toBeNull(); + }); + + it('labels the state machine action of state errors', () => { + showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]); + + expect(root.querySelector('.diagnostic-state-machine-btn')?.textContent?.trim()).toBe('Show in state machine'); + expect(root.querySelector('.diagnostic-actions .diagnostic-state-machine-btn')).toBeNull(); + }); + it('toggles between file and workspace errors by clicking scope buttons', () => { showDiagnostics([ diagnostic(currentFile, 'Current error'), diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 3fe2fa8..c44ff84 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"; @@ -12,7 +12,8 @@ import { copyDiagnosticToClipboard, getDisplayDiagnostics, renderDiagnosticsView 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 { getDiagnosticRevealTarget, getDiagnosticRevealTargetFromKey, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; +import { findStateError, getAllStateErrors, getStateErrorKey, getStateErrors } from "./state-errors"; type VSCodeApi = { postMessage(message: unknown): void; @@ -31,8 +32,9 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let showAllDiagnostics = false; let currentFile: string; let stateMachine: LJStateMachine | undefined; - let diagnosticStateMachine: LJStateMachine | undefined; - let diagnosticStateMachineFile: string | undefined; + // the last state error shown, kept while switching tabs + let selectedStateError: StateRefinementError | undefined; + let cursorStateErrorKey: string | undefined; let context: LJContext; let errorAtCursor: RefinementMismatchError; let selectedTab: NavTab = 'diagnostics'; @@ -41,6 +43,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let showDiagramConditions = false; let focusDiagramOnError = false; let currentDiagram: string = ''; + let renderedStateMachineView: string | undefined; let revealTimeout: ReturnType | undefined; const contextSectionState: ContextSectionState = { aliases: false, @@ -143,15 +146,34 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const diagnostic = getDisplayDiagnostics(diagnostics ?? [], showAllDiagnostics, currentFile) .filter(d => d.category === 'error')[errorIndex]; if (diagnostic?.type !== 'state-refinement-error' || !diagnostic.stateMachine) return; + showStateError(diagnostic); + return; + } - selectedTab = 'fsm'; - diagnosticStateMachine = diagnostic.stateMachine; - diagnosticStateMachineFile = diagnostic.file; - showDiagramConditions = false; - focusDiagramOnError = true; - resetZoom(document); - currentDiagram = ''; - updateView(); + // step through the state errors of the current file + const stateErrorStepButton = target.closest?.('.state-error-step-btn'); + if (stateErrorStepButton) { + e.stopPropagation(); + if ((stateErrorStepButton as HTMLButtonElement).disabled) return; + const errors = getCurrentStateErrors(); + const index = getShownStateErrorIndex(errors) + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10); + if (errors[index]) showStateError(errors[index]); + return; + } + + // show the first state error of the current file + if (target.closest?.('#state-error-show-btn')) { + e.stopPropagation(); + const [first] = getCurrentStateErrors(); + if (first) showStateError(first); + return; + } + + // go back to the shown state error in the Verification tab + if (target.closest?.('#state-error-reveal-btn')) { + e.stopPropagation(); + const revealTarget = selectedStateError && getDiagnosticRevealTarget(selectedStateError); + if (revealTarget) revealDiagnostic(revealTarget); return; } @@ -281,10 +303,6 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) const tab = target.getAttribute('data-tab') as NavTab; if (tab && tab !== selectedTab) { vscode.postMessage({ type: 'highlight', range: null }); - if (tab === 'fsm') { - diagnosticStateMachine = undefined; - diagnosticStateMachineFile = undefined; - } selectedTab = tab; updateView(); } @@ -351,42 +369,36 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) updateView(); break; case 'diagnostics': { + const previousErrors = getAllStateErrors(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 }; - } - if (selectedTab === 'diagnostics' || (selectedTab === 'fsm' && diagnosticStateMachine)) updateView(); + selectedStateError = findStateError(getAllStateErrors(diagnostics), selectedStateError, previousErrors); + if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); + else updateView(); break; } case 'file': currentFile = msg.file; if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView(); - diagnosticStateMachine = undefined; - diagnosticStateMachineFile = undefined; stateMachine = undefined; - currentDiagram = ''; - if (selectedTab === 'fsm') updateView(); + if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); break; case 'fsm': stateMachine = (msg.sm as LJStateMachine | null) ?? undefined; - showDiagramConditions = false; - if (selectedTab === 'fsm' && !diagnosticStateMachine) updateView(); + if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); break; case 'context': context = msg.context as LJContext; errorAtCursor = msg.errorAtCursor as RefinementMismatchError; + followCursorStateError(msg.errorAtCursor as LJDiagnostic | undefined); if (selectedTab === 'context') updateView(); break; - case 'revealDiagnostic': - revealDiagnostic(msg.diagnostic as DiagnosticRevealTarget); + case 'revealDiagnostic': { + const revealTarget = msg.diagnostic as DiagnosticRevealTarget; + const stateError = msg.tab === 'fsm' ? findStateErrorAt(revealTarget) : undefined; + if (stateError) showStateError(stateError); + else revealDiagnostic(revealTarget); break; + } } }); @@ -405,30 +417,90 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) return; } + const stateErrors = getCurrentStateErrors(); + renderedStateMachineView = undefined; switch (selectedTab) { case 'diagnostics': root.innerHTML = diagnostics - ? renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile) + ? renderDiagnosticsView(diagnostics, showAllDiagnostics, currentFile, stateErrors.length) : renderLoading(); break; case 'fsm': { - const displayedStateMachine = diagnosticStateMachine ?? stateMachine; - const focusOnError = focusDiagramOnError && !!diagnosticStateMachine; + const shownIndex = getShownStateErrorIndex(stateErrors); + const shownError = stateErrors[shownIndex]; + const displayedStateMachine = shownError?.stateMachine ?? stateMachine; + const focusOnError = focusDiagramOnError && !!shownError; const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions, focusOnError); // copy the diagram without the error overlay currentDiagram = displayedStateMachine?.errorContext ? createMermaidDiagram({ ...displayedStateMachine, errorContext: null }, diagramOrientation, showDiagramConditions) : diagram; - renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError); + renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError, + { index: shownIndex, count: stateErrors.length }); + renderedStateMachineView = getStateMachineViewKey(); if (displayedStateMachine) renderMermaidDiagram(document, window); break; } case 'context': - root.innerHTML = renderContextView(context, currentFile, contextSectionState, errorAtCursor); + root.innerHTML = renderContextView(context, currentFile, contextSectionState, errorAtCursor, stateErrors.length); break; } } + function getCurrentStateErrors(): StateRefinementError[] { + return getStateErrors(diagnostics, currentFile, stateMachine); + } + + function getShownStateErrorIndex(errors: StateRefinementError[]): number { + if (!selectedStateError) return -1; + const key = getStateErrorKey(selectedStateError); + return errors.findIndex(error => getStateErrorKey(error) === key); + } + + function findStateErrorAt(target: DiagnosticRevealTarget): StateRefinementError | undefined { + const key = getDiagnosticRevealTargetKey(target); + return getAllStateErrors(diagnostics).find(error => getStateErrorKey(error) === key); + } + + function showStateError(error: StateRefinementError) { + selectedTab = 'fsm'; + selectedStateError = error; + showDiagramConditions = false; + focusDiagramOnError = true; + resetZoom(document); + currentDiagram = ''; + updateView(); + } + + // shows the state error at the cursor once the cursor reaches it, without overriding later choices in the view + function followCursorStateError(error: LJDiagnostic | undefined) { + const stateError = error?.type === 'state-refinement-error' && error.stateMachine ? error : undefined; + const key = stateError ? getStateErrorKey(stateError) : undefined; + if (key === cursorStateErrorKey) return; + cursorStateErrorKey = key; + if (!stateError || (selectedStateError && getStateErrorKey(selectedStateError) === key)) return; + if (selectedTab === 'fsm') { + showStateError(stateError); + } else { + selectedStateError = stateError; + focusDiagramOnError = true; + } + } + + // a new verification or file only re-renders the diagram when what it shows changed, so panning and focus are kept + function updateStateMachineViewIfChanged() { + if (status !== 'loading' && status !== 'stopped' && status !== 'crashed' + && renderedStateMachineView === getStateMachineViewKey()) return; + currentDiagram = ''; + updateView(); + } + + function getStateMachineViewKey(): string { + const stateErrors = getCurrentStateErrors(); + const shownError = stateErrors[getShownStateErrorIndex(stateErrors)]; + return JSON.stringify([shownError?.stateMachine ?? stateMachine ?? null, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]); + } + function revealDiagnostic(target: DiagnosticRevealTarget) { selectedTab = 'diagnostics'; diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts new file mode 100644 index 0000000..2db1705 --- /dev/null +++ b/client/src/webview/state-errors.spec.ts @@ -0,0 +1,92 @@ +import { describe, expect, it } from 'vitest'; +import type { LJDiagnostic, StateRefinementError } from '../types/diagnostics'; +import type { LJStateMachine } from '../types/fsm'; +import { findStateError, getAllStateErrors, getStateErrorKey, getStateErrors } from './state-errors'; + +const refinementsFile = '/workspace/src/DefaultMutableTreeNodeRefinements.java'; +const callerFile = '/workspace/src/OutlineBuilder.java'; +const otherCallerFile = '/workspace/src/Another.java'; + +function machine(className = 'javax.swing.tree.DefaultMutableTreeNode'): LJStateMachine { + return { + className, states: ['childrenAllowed', 'maybeHasChildren'], + initialTransitions: [{ to: 'childrenAllowed' }], + transitions: [{ from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }], + errorContext: { calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'] }, + }; +} + +function stateError(line: number, overrides: Partial = {}): StateRefinementError { + const file = overrides.file ?? callerFile; + return { + category: 'error', type: 'state-refinement-error', title: 'State Refinement Error', + message: 'found childrenAllowed(root¹⁸) but expected maybeHasChildren(root¹⁸)', hint: null, + file, position: { file, lineStart: line, colStart: 15, lineEnd: line, colEnd: 35 }, + translationTable: {}, expected: 'maybeHasChildren(root¹⁸)', + found: { implication: null as never, origin: null, simplification: null }, + customMessage: '', + declarationPosition: { file: refinementsFile, lineStart: 21, colStart: 29, lineEnd: 21, colEnd: 51 }, + stateMachine: machine(), + ...overrides, + }; +} + +describe('state errors', () => { + it('keeps only the state errors that carry a state machine', () => { + const withMachine = stateError(10); + const withoutMachine = stateError(14, { stateMachine: null }); + const refinementError = { ...stateError(16), type: 'custom-error' } as unknown as LJDiagnostic; + + expect(getAllStateErrors([withMachine, withoutMachine, refinementError])).toEqual([withMachine]); + expect(getAllStateErrors(undefined)).toEqual([]); + }); + + it('lists the errors of the current file in source order', () => { + const later = stateError(20); + const earlier = stateError(10); + const otherFile = stateError(5, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') }); + + expect(getStateErrors([later, otherFile, earlier], callerFile, undefined)).toEqual([earlier, later]); + expect(getStateErrors([later], undefined, undefined)).toEqual([]); + }); + + it('adds the errors on the state machine of the current file from other files after its own', () => { + const ownError = stateError(30, { file: refinementsFile, stateMachine: machine('java.util.ArrayList') }); + const callerError = stateError(10); + const otherCallerError = stateError(4, { file: otherCallerFile }); + const otherMachine = stateError(2, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') }); + + expect(getStateErrors([callerError, otherMachine, otherCallerError, ownError], refinementsFile, machine())) + .toEqual([ownError, otherCallerError, callerError]); + }); + + 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, [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(); + }); +}); diff --git a/client/src/webview/state-errors.ts b/client/src/webview/state-errors.ts new file mode 100644 index 0000000..25ae096 --- /dev/null +++ b/client/src/webview/state-errors.ts @@ -0,0 +1,68 @@ +import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics"; +import type { LJStateMachine } from "../types/fsm"; +import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; + +/** + * Gets the state errors that the State Machine view can show for the current file + * These are the state errors reported in the file and, since errors are usually reported in the caller file, + * the ones on the state machine declared in the file, with the errors of the file first in source order + * @param diagnostics All diagnostics in the workspace + * @param currentFile The file open in the editor + * @param sm The state machine declared in the current file + */ +export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined, sm: LJStateMachine | undefined): StateRefinementError[] { + const isCurrentFile = (error: StateRefinementError) => !!currentFile && error.file.toLowerCase() === currentFile.toLowerCase(); + return getAllStateErrors(diagnostics) + .filter(error => isCurrentFile(error) || error.stateMachine?.className === sm?.className) + .map((error, index) => ({ error, index })) + .sort((a, b) => Number(isCurrentFile(b.error)) - Number(isCurrentFile(a.error)) + || a.error.file.localeCompare(b.error.file) + || (a.error.position?.lineStart ?? 0) - (b.error.position?.lineStart ?? 0) + || (a.error.position?.colStart ?? 0) - (b.error.position?.colStart ?? 0) + || a.index - b.index) + .map(({ error }) => error); +} + +/** + * Gets the state errors in the workspace that carry the state machine of their receiver + * @param diagnostics All diagnostics in the workspace + */ +export function getAllStateErrors(diagnostics: LJDiagnostic[] | undefined): StateRefinementError[] { + return (diagnostics ?? []).filter((diagnostic): diagnostic is StateRefinementError => + diagnostic.type === 'state-refinement-error' && !!diagnostic.stateMachine); +} + +export function getStateErrorKey(error: StateRefinementError): string { + const target = getDiagnosticRevealTarget(error); + // 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 + * 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 state errors after the verification + * @param selected The previously selected error + * @param previousErrors The state errors before the verification + */ +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 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 { + const position = error.declarationPosition; + if (!position?.file) return undefined; + return getDiagnosticRevealTargetKey({ file: position.file, position }); +} diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 9eabf6c..1042810 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -144,6 +144,20 @@ export function getStyles(): string { opacity: 1; background: none; } + .nav-badge { + display: inline-block; + min-width: 1rem; + margin-left: 0.2rem; + padding: 0 0.25rem; + box-sizing: border-box; + color: var(--vscode-editor-background); + background: var(--vscode-errorForeground); + border-radius: 0.5rem; + font-size: 10px; + font-weight: 600; + line-height: 1rem; + text-align: center; + } .container { margin: 0; padding: 0.5rem; @@ -189,8 +203,7 @@ export function getStyles(): string { gap: 0.25rem; } .copy-diagnostic-btn, - .diagnostic-context-btn, - .diagnostic-state-machine-btn { + .diagnostic-context-btn { display: inline-flex; align-items: center; justify-content: center; @@ -225,18 +238,29 @@ export function getStyles(): string { pointer-events: none; } .copy-diagnostic-btn:hover, - .diagnostic-context-btn:hover, - .diagnostic-state-machine-btn:hover { + .diagnostic-context-btn:hover { background: var(--vscode-editor-background); border-color: var(--vscode-widget-border); opacity: 1; } .copy-diagnostic-btn:disabled, - .diagnostic-context-btn:disabled, - .diagnostic-state-machine-btn:disabled { + .diagnostic-context-btn:disabled { opacity: 0.8; cursor: default; } + .diagnostic-state-machine-btn { + display: inline-flex; + align-items: center; + gap: 0.4rem; + margin: 0.75rem 0 0.25rem; + padding: 0.25rem 0.6rem; + color: var(--vscode-button-secondaryForeground); + background-color: var(--vscode-button-secondaryBackground); + font-size: 0.85rem; + } + .diagnostic-state-machine-btn:hover { + background-color: var(--vscode-button-secondaryHoverBackground); + } .icon-button-pop { animation: icon-button-pop 0.28s ease-out; } @@ -1072,6 +1096,31 @@ export function getStyles(): string { .diagram-focus-btn { flex-shrink: 0; } + .diagram-error-actions { + display: flex; + flex-wrap: wrap; + align-items: center; + gap: 0.25rem 0.75rem; + } + .state-error-stepper { + display: inline-flex; + align-items: center; + } + .state-error-position { + white-space: nowrap; + font-variant-numeric: tabular-nums; + } + .state-error-reveal-btn { + padding: 0; + color: var(--vscode-textLink-foreground); + background: none; + border: none; + font-size: inherit; + } + .state-error-reveal-btn:hover { + background: none; + text-decoration: underline; + } .diagram-error-legend { display: flex; flex-wrap: wrap; diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts index 833ab3f..2539d41 100644 --- a/client/src/webview/views/context/context.ts +++ b/client/src/webview/views/context/context.ts @@ -11,14 +11,14 @@ export type ContextSectionState = { vars: boolean; } -export function renderContextView(context: LJContext | undefined, currentFile: string | undefined, sectionState: ContextSectionState, errorAtCursor?: RefinementMismatchError): string { +export function renderContextView(context: LJContext | undefined, currentFile: string | undefined, sectionState: ContextSectionState, errorAtCursor?: RefinementMismatchError, stateErrorCount = 0): string { const allVars = context?.allVars || []; const ghosts = context?.ghosts?.filter(ghost => ghost.file === currentFile) || []; const aliases = context?.aliases || []; const total = allVars.length + ghosts.length + aliases.length; return /*html*/`
- ${renderMainHeader("", 'context')} + ${renderMainHeader("", 'context', stateErrorCount)} ${total === 0 ? 'No context information available at the cursor position' : `${renderContextAliases(aliases, sectionState.aliases)} diff --git a/client/src/webview/views/diagnostics/diagnostics.ts b/client/src/webview/views/diagnostics/diagnostics.ts index 92332ac..d6efabb 100644 --- a/client/src/webview/views/diagnostics/diagnostics.ts +++ b/client/src/webview/views/diagnostics/diagnostics.ts @@ -11,6 +11,7 @@ export function renderDiagnosticsView( diagnostics: LJDiagnostic[], showAll: boolean, currentFile: string | undefined, + stateErrorCount = 0, ): string { const fileDiagnostics = diagnostics.filter(diagnostic => diagnostic.file?.toLowerCase() === currentFile?.toLowerCase() || !diagnostic.file); const displayDiagnostics = showAll ? diagnostics : fileDiagnostics; @@ -32,7 +33,7 @@ export function renderDiagnosticsView( return /*html*/`
- ${renderMainHeader(hasErrors ? "" : "Passed Verification", 'diagnostics')} + ${renderMainHeader(hasErrors ? "" : "Passed Verification", 'diagnostics', stateErrorCount)} ${scopeSelector} ${!hasErrors ? '

No errors were found by the LiquidJava verifier.

' : ''} ${ diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 126b24e..0058d67 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -22,11 +22,11 @@ export function renderErrors(errors: LJError[]): string { return /*html*/`
  • - ${renderDiagnosticStateMachineAction(error, index)} ${renderDiagnosticContextAction(error)} ${renderCopyDiagnosticButton('error', index)}
    ${renderError(error)} + ${renderDiagnosticStateMachineAction(error, index)}
    • `; }).join("")} diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index f17d6e5..95a6d5d 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -223,4 +223,50 @@ describe('state machine view', () => { expect(container.style.minHeight).toBe('240px'); expect(document.querySelector('.diagram-title')?.textContent).toBe('UpdatedConnection'); }); + + it('steps through several state errors and links back to the shown one', () => { + const errorMachine = machine({ + errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + }); + const stepButtons = () => Array.from(document.querySelectorAll('.state-error-step-btn'), + node => [node.getAttribute('aria-label'), node.disabled]); + + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 }); + expect(document.querySelector('.state-error-position')?.textContent).toBe('1 of 3'); + expect(stepButtons()).toEqual([['Previous state error', true], ['Next state error', false]]); + expect(button('state-error-reveal-btn').textContent).toBe('View error'); + expect(document.querySelector('.nav-tab.selected .nav-badge')?.textContent).toBe('3'); + + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 2, count: 3 }); + expect(document.querySelector('.state-error-position')?.textContent).toBe('3 of 3'); + expect(stepButtons()).toEqual([['Previous state error', false], ['Next state error', true]]); + + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 1 }); + expect(document.querySelector('.state-error-stepper')).toBeNull(); + expect(button('state-error-reveal-btn')).not.toBeNull(); + }); + + it.each([ + ['the file state machine', machine()], + ['no state machine', undefined], + ])('points to the state errors of the file when none is shown, with %s', (_, sm) => { + renderStateMachineView(document.body, sm, sm ? diagram : '', 'TB', false, false, { index: -1, count: 2 }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe('2 state errors found'); + expect(button('state-error-show-btn').textContent).toBe('Show first'); + expect(document.querySelector('#diagram-focus-btn')).toBeNull(); + expect(document.querySelector('.nav-badge')?.textContent).toBe('2'); + expect(document.body.textContent).not.toContain('No state machine available'); + + renderStateMachineView(document.body, sm, sm ? diagram : '', 'TB', false, false, { index: -1, count: 1 }); + expect(document.querySelector('.diagram-error-text')?.textContent).toBe('1 state error found'); + expect(button('state-error-show-btn').textContent).toBe('Show error'); + }); + + it('shows no state error badge or hint when the file has no state errors', () => { + renderStateMachineView(document.body, machine(), diagram, 'TB', false, false, { index: -1, count: 0 }); + + expect(document.querySelector('.nav-badge')).toBeNull(); + expect(document.querySelector('.diagram-error-summary')).toBeNull(); + }); }); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index 69904d2..db190ba 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -4,14 +4,27 @@ 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, focusOnError = false) { +/** + * The position of the shown state error among the state errors of the current file + * The index is -1 when none of them is shown + */ +export type StateErrorNavigation = { + index: number; + count: number; +}; + +// shows the error context of the machine, if any, without stepping through errors +const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: 0, count: 0 }; + +export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION) { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; const diagramHeight = previousDiagramContainer?.offsetHeight; - root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, focusOnError, diagramHeight); + root.innerHTML = renderStateMachineViewHtml(sm, diagram, orientation, showConditions, focusOnError, stateErrors, diagramHeight); } -function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, diagramHeight?: number): string { - const errorFocus = getStateErrorFocus(sm); +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string { + const errorFocus = stateErrors.index >= 0 ? getStateErrorFocus(sm) : null; + const hiddenErrors = stateErrors.index < 0 ? renderHiddenStateErrors(stateErrors.count) : ''; const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.toCondition) || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition) @@ -22,7 +35,8 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
    - ${renderMainHeader("", 'fsm')} + ${renderMainHeader("", 'fsm', stateErrors.count)} + ${!sm ? hiddenErrors : ''} ${sm ? /*html*/`
    @@ -37,7 +51,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
    - ${errorFocus ? renderStateErrorSummary(errorFocus, focusOnError) + renderStateErrorLegend(errorFocus) : ''} + ${errorFocus ? renderStateErrorSummary(errorFocus, focusOnError, stateErrors) + renderStateErrorLegend(errorFocus) : hiddenErrors} ${showConditions && hasConditionExpansions ? /*html*/`
    Precondition @@ -51,12 +65,12 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
    ` - : 'No state machine available for the current file'} + : hiddenErrors ? '' : 'No state machine available for the current file'}
    `; } -function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean): string { +function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean, stateErrors: StateErrorNavigation): string { const call = getRejectedCallText(focus); const receiver = focus.receiver ? `${escapeHtml(focus.receiver)}` : 'the receiver'; const rejected = `${call ? `${escapeHtml(call)}` : 'The call'} is rejected`; @@ -73,9 +87,34 @@ function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean): return /*html*/`

    ${summary}

    - +
    + ${stateErrors.count > 1 ? renderStateErrorStepper(stateErrors) : ''} + + +
    +
    + `; +} + +function renderStateErrorStepper({ index, count }: StateErrorNavigation): string { + return /*html*/` + + ${renderCodiconButton("chevron-left", { className: "diagram-control-btn state-error-step-btn", title: "Previous state error", attributes: 'data-step="-1"', disabled: index <= 0 })} + ${index + 1} of ${count} + ${renderCodiconButton("chevron-right", { className: "diagram-control-btn state-error-step-btn", title: "Next state error", attributes: 'data-step="1"', disabled: index >= count - 1 })} + + `; +} + +// points to the state errors of the current file when none of them is shown +function renderHiddenStateErrors(count: number): string { + if (count === 0) return ''; + return /*html*/` +
    +

    ${count} state error${count === 1 ? '' : 's'} found

    +
    `; } diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index df94ec5..de512f5 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -5,9 +5,9 @@ import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "../diag import { renderCodicon, renderCodiconButton } from "../icons"; import { LJVariable } from "../../types/context"; -export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/` +export const renderMainHeader = (title: string, selectedTab: NavTab, stateErrorCount = 0): string => /*html*/`
    - ${renderNav(selectedTab)} + ${renderNav(selectedTab, stateErrorCount)}

    ${title}

    `; @@ -97,12 +97,11 @@ export function renderDiagnosticContextButton(position?: SourcePosition | null): } export function renderDiagnosticStateMachineButton(errorIndex: number): string { - return renderCodiconButton("type-hierarchy", { - className: "diagnostic-state-machine-btn", - title: "View error on state machine", - attributes: `data-error-index="${errorIndex}"`, - errorBadge: true, - }); + return /*html*/` + + `; } export function renderDiagnosticRevealButton(position: SourcePosition, content: string): string { @@ -134,13 +133,16 @@ function getFile(position: SourcePosition): string { export type NavTab = 'diagnostics' | 'fsm' | 'context'; -export function renderNav(selectedTab: NavTab): string { +export function renderNav(selectedTab: NavTab, stateErrorCount = 0): string { + const stateErrorBadge = stateErrorCount > 0 + ? ` ${stateErrorCount}` + : ''; return /*html*/` `; 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 f3e6ebaa0bf114e52a47da41d0a0debb7df8c121 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 00:55:19 +0100 Subject: [PATCH 2/3] Open the State Machine view on the first state error of the file Count only the state errors of the current file, keep the focus toggle with the legend apart from View error, and move Show in state machine to the top of the error. Co-Authored-By: Claude Opus 5.5 --- client/media/walkthrough/state-machine.md | 2 +- client/package.json | 2 +- client/src/webview/script.spec.ts | 45 +++++++++++++++---- client/src/webview/script.ts | 34 +++++++------- client/src/webview/state-errors.spec.ts | 17 ++----- client/src/webview/state-errors.ts | 17 +++---- client/src/webview/styles.ts | 4 +- .../src/webview/views/diagnostics/errors.ts | 12 +++-- client/src/webview/views/fsm/fsm.spec.ts | 30 +++++++------ client/src/webview/views/fsm/fsm.ts | 45 +++++++------------ 10 files changed, 109 insertions(+), 99 deletions(-) diff --git a/client/media/walkthrough/state-machine.md b/client/media/walkthrough/state-machine.md index a73bcfb..94bcdb9 100644 --- a/client/media/walkthrough/state-machine.md +++ b/client/media/walkthrough/state-machine.md @@ -1,4 +1,4 @@ The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`. Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it. Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition. -From a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it. +From a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it. diff --git a/client/package.json b/client/package.json index cb02075..03c22c5 100644 --- a/client/package.json +++ b/client/package.json @@ -240,7 +240,7 @@ { "id": "stateMachine", "title": "Explore state machines", - "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)", + "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { "markdown": "media/walkthrough/state-machine.md" }, diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index a45c230..bfe2ed1 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -57,10 +57,10 @@ const stateMachine: LJStateMachine = { errorContext: null, }; -function stateError(title: string, sm: LJStateMachine, line = position.lineStart): LJDiagnostic { - const errorPosition = { ...position, lineStart: line, lineEnd: line }; +function stateError(title: string, sm: LJStateMachine, line = position.lineStart, file = currentFile): LJDiagnostic { + const errorPosition = { ...position, file, lineStart: line, lineEnd: line }; return { - title, message: `${title} message`, hint: null, file: currentFile, position: errorPosition, + title, message: `${title} message`, hint: null, file, position: errorPosition, category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)', found: { implication: null as never, origin: null, simplification: 'Closed(counter)' }, customMessage: '', declarationPosition: null, stateMachine: sm, @@ -285,16 +285,28 @@ describe('webview script', () => { expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); }); - it('points to the state errors of the file until one is shown', () => { - showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]); + it('opens on the first state error of the file, focused', () => { + showDiagnostics([ + stateError('Second state error', errorMachine('Second', 'reset'), 9), + stateError('First state error', errorMachine('First', 'close'), 4), + ]); receive({ type: 'fsm', sm: stateMachine }); click('[data-tab="fsm"]'); - expect(root.querySelector('.diagram-error-text')?.textContent).toBe('1 state error found'); - expect(root.querySelector('.mermaid')?.textContent).not.toContain('ljState'); - click('#state-error-show-btn'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('First'); + expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2'); expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all'); - expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed'); + expect(root.querySelector('.mermaid')?.textContent).toContain('ljStateDimmed'); + }); + + it('counts only the state errors of the current file, as listed in the Verification tab', () => { + showDiagnostics([ + stateError('State refinement error', errorMachine('Counter', 'close'), 4), + stateError('Other file error', errorMachine('Counter', 'close'), 2, otherFile), + ]); + + expect(root.querySelector('[data-tab="fsm"] .nav-badge')?.textContent).toBe('1'); + expect(root.querySelectorAll('.diagnostic-state-machine-btn')).toHaveLength(1); }); it('follows the state error at the cursor without overriding a later choice', () => { @@ -368,6 +380,21 @@ describe('webview script', () => { expect(root.querySelector('.diagnostic-state-machine-btn')?.textContent?.trim()).toBe('Show in state machine'); expect(root.querySelector('.diagnostic-actions .diagnostic-state-machine-btn')).toBeNull(); + // right below the error message, before its details + const firstSection = root.querySelector('.error-item .section')!; + expect(root.querySelector('.diagnostic-state-machine-btn')!.compareDocumentPosition(firstSection)).toBe(Node.DOCUMENT_POSITION_FOLLOWING); + }); + + it('opens on the first state error of a newly opened file', () => { + showDiagnostics([ + stateError('Main error', errorMachine('Main', 'close'), 4), + stateError('Other file error', errorMachine('Other', 'close'), 2, otherFile), + ]); + click('.diagnostic-state-machine-btn'); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Main'); + + receive({ type: 'file', file: otherFile }); + expect(root.querySelector('.diagram-title')?.textContent).toBe('Other'); }); it('toggles between file and workspace errors by clicking scope buttons', () => { diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index c44ff84..6dcb6f5 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -41,7 +41,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) let status: ExtensionStatus = 'loading'; let diagramOrientation: "LR" | "TB" = "TB"; let showDiagramConditions = false; - let focusDiagramOnError = false; + let focusDiagramOnError = true; let currentDiagram: string = ''; let renderedStateMachineView: string | undefined; let revealTimeout: ReturnType | undefined; @@ -156,23 +156,16 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) e.stopPropagation(); if ((stateErrorStepButton as HTMLButtonElement).disabled) return; const errors = getCurrentStateErrors(); - const index = getShownStateErrorIndex(errors) + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10); + const index = getShownStateError(errors).index + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10); if (errors[index]) showStateError(errors[index]); return; } - // show the first state error of the current file - if (target.closest?.('#state-error-show-btn')) { - e.stopPropagation(); - const [first] = getCurrentStateErrors(); - if (first) showStateError(first); - return; - } - // go back to the shown state error in the Verification tab if (target.closest?.('#state-error-reveal-btn')) { e.stopPropagation(); - const revealTarget = selectedStateError && getDiagnosticRevealTarget(selectedStateError); + const { error } = getShownStateError(getCurrentStateErrors()); + const revealTarget = error && getDiagnosticRevealTarget(error); if (revealTarget) revealDiagnostic(revealTarget); return; } @@ -378,6 +371,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } case 'file': currentFile = msg.file; + // the view shows the first error of the new file instead + if (selectedStateError && selectedStateError.file.toLowerCase() !== currentFile?.toLowerCase()) selectedStateError = undefined; if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView(); stateMachine = undefined; if (selectedTab === 'fsm') updateStateMachineViewIfChanged(); @@ -426,8 +421,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) : renderLoading(); break; case 'fsm': { - const shownIndex = getShownStateErrorIndex(stateErrors); - const shownError = stateErrors[shownIndex]; + const { error: shownError, index: shownIndex } = getShownStateError(stateErrors); const displayedStateMachine = shownError?.stateMachine ?? stateMachine; const focusOnError = focusDiagramOnError && !!shownError; const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions, focusOnError); @@ -448,13 +442,17 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } function getCurrentStateErrors(): StateRefinementError[] { - return getStateErrors(diagnostics, currentFile, stateMachine); + return getStateErrors(diagnostics, currentFile); } - function getShownStateErrorIndex(errors: StateRefinementError[]): number { - if (!selectedStateError) return -1; + /** + * Gets the state error the view shows and its index among the state errors of the current file + * This is the selected error, which is outside them when chosen from another file, or else the first one + */ + function getShownStateError(errors: StateRefinementError[]): { error: StateRefinementError | undefined; index: number } { + if (!selectedStateError) return { error: errors[0], index: errors.length > 0 ? 0 : -1 }; const key = getStateErrorKey(selectedStateError); - return errors.findIndex(error => getStateErrorKey(error) === key); + return { error: selectedStateError, index: errors.findIndex(error => getStateErrorKey(error) === key) }; } function findStateErrorAt(target: DiagnosticRevealTarget): StateRefinementError | undefined { @@ -497,7 +495,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) function getStateMachineViewKey(): string { const stateErrors = getCurrentStateErrors(); - const shownError = stateErrors[getShownStateErrorIndex(stateErrors)]; + const { error: shownError } = getShownStateError(stateErrors); return JSON.stringify([shownError?.stateMachine ?? stateMachine ?? null, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]); } diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index 2db1705..567baf6 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -44,20 +44,11 @@ describe('state errors', () => { it('lists the errors of the current file in source order', () => { const later = stateError(20); const earlier = stateError(10); - const otherFile = stateError(5, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') }); + const otherFile = stateError(5, { file: otherCallerFile }); - expect(getStateErrors([later, otherFile, earlier], callerFile, undefined)).toEqual([earlier, later]); - expect(getStateErrors([later], undefined, undefined)).toEqual([]); - }); - - it('adds the errors on the state machine of the current file from other files after its own', () => { - const ownError = stateError(30, { file: refinementsFile, stateMachine: machine('java.util.ArrayList') }); - const callerError = stateError(10); - const otherCallerError = stateError(4, { file: otherCallerFile }); - const otherMachine = stateError(2, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') }); - - expect(getStateErrors([callerError, otherMachine, otherCallerError, ownError], refinementsFile, machine())) - .toEqual([ownError, otherCallerError, callerError]); + expect(getStateErrors([later, otherFile, earlier], callerFile)).toEqual([earlier, later]); + expect(getStateErrors([later, otherFile], refinementsFile)).toEqual([]); + expect(getStateErrors([later], undefined)).toEqual([]); }); it('finds the selected error again after verification', () => { diff --git a/client/src/webview/state-errors.ts b/client/src/webview/state-errors.ts index 25ae096..88e7a19 100644 --- a/client/src/webview/state-errors.ts +++ b/client/src/webview/state-errors.ts @@ -1,23 +1,18 @@ import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics"; -import type { LJStateMachine } from "../types/fsm"; import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; /** - * Gets the state errors that the State Machine view can show for the current file - * These are the state errors reported in the file and, since errors are usually reported in the caller file, - * the ones on the state machine declared in the file, with the errors of the file first in source order + * Gets the state errors reported in the current file, in source order + * These are the errors the State Machine view steps through, one for each Show in state machine button of the file * @param diagnostics All diagnostics in the workspace * @param currentFile The file open in the editor - * @param sm The state machine declared in the current file */ -export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined, sm: LJStateMachine | undefined): StateRefinementError[] { - const isCurrentFile = (error: StateRefinementError) => !!currentFile && error.file.toLowerCase() === currentFile.toLowerCase(); +export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined): StateRefinementError[] { + if (!currentFile) return []; return getAllStateErrors(diagnostics) - .filter(error => isCurrentFile(error) || error.stateMachine?.className === sm?.className) + .filter(error => error.file.toLowerCase() === currentFile.toLowerCase()) .map((error, index) => ({ error, index })) - .sort((a, b) => Number(isCurrentFile(b.error)) - Number(isCurrentFile(a.error)) - || a.error.file.localeCompare(b.error.file) - || (a.error.position?.lineStart ?? 0) - (b.error.position?.lineStart ?? 0) + .sort((a, b) => (a.error.position?.lineStart ?? 0) - (b.error.position?.lineStart ?? 0) || (a.error.position?.colStart ?? 0) - (b.error.position?.colStart ?? 0) || a.index - b.index) .map(({ error }) => error); diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts index 1042810..abef3e0 100644 --- a/client/src/webview/styles.ts +++ b/client/src/webview/styles.ts @@ -252,7 +252,7 @@ export function getStyles(): string { display: inline-flex; align-items: center; gap: 0.4rem; - margin: 0.75rem 0 0.25rem; + margin: 0 0 1rem; padding: 0.25rem 0.6rem; color: var(--vscode-button-secondaryForeground); background-color: var(--vscode-button-secondaryBackground); @@ -1095,6 +1095,7 @@ export function getStyles(): string { } .diagram-focus-btn { flex-shrink: 0; + margin-left: auto; } .diagram-error-actions { display: flex; @@ -1124,6 +1125,7 @@ export function getStyles(): string { .diagram-error-legend { display: flex; flex-wrap: wrap; + align-items: center; gap: 0.25rem 1rem; margin-bottom: 0.75rem; font-size: 0.8rem; diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts index 0058d67..1b9db34 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -25,8 +25,7 @@ export function renderErrors(errors: LJError[]): string { ${renderDiagnosticContextAction(error)} ${renderCopyDiagnosticButton('error', index)} - ${renderError(error)} - ${renderDiagnosticStateMachineAction(error, index)} + ${renderError(error, renderDiagnosticStateMachineAction(error, index))} `; }).join("")} @@ -67,13 +66,18 @@ const errorContentRenderers: ErrorRendererMap = { 'custom-error': (_: CustomError) => "", }; -export function renderError(error: LJError): string { +/** + * Renders the error content + * @param error The error to render + * @param headerActions Actions shown below the error message + */ +export function renderError(error: LJError, headerActions = ''): string { const message = error.type === 'refinement-error' || error.type === 'state-refinement-error' ? error.customMessage : error.message; const header = renderDiagnosticHeader(error.title, message || ''); const content = (errorContentRenderers[error.type] as (error: LJError) => string)?.(error) || ''; const hint = renderHint(error.hint); const location = renderLocation(error); - return /*html*/`${header}${content}${hint}${location}`; + return /*html*/`${header}${headerActions}${content}${hint}${location}`; } function renderDiagnosticContextAction(error: LJError): string { diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 95a6d5d..c3207b8 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -246,24 +246,28 @@ describe('state machine view', () => { expect(button('state-error-reveal-btn')).not.toBeNull(); }); - it.each([ - ['the file state machine', machine()], - ['no state machine', undefined], - ])('points to the state errors of the file when none is shown, with %s', (_, sm) => { - renderStateMachineView(document.body, sm, sm ? diagram : '', 'TB', false, false, { index: -1, count: 2 }); + it('shows an error chosen from another file without stepping through the errors of the file', () => { + const errorMachine = machine({ + errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + }); + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: -1, count: 2 }); - expect(document.querySelector('.diagram-error-text')?.textContent).toBe('2 state errors found'); - expect(button('state-error-show-btn').textContent).toBe('Show first'); - expect(document.querySelector('#diagram-focus-btn')).toBeNull(); + expect(document.querySelector('.state-error-stepper')).toBeNull(); + expect(button('state-error-reveal-btn')).not.toBeNull(); expect(document.querySelector('.nav-badge')?.textContent).toBe('2'); - expect(document.body.textContent).not.toContain('No state machine available'); + }); + + it('keeps the focus toggle with the legend, apart from the error actions', () => { + const errorMachine = machine({ + errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + }); + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 }); - renderStateMachineView(document.body, sm, sm ? diagram : '', 'TB', false, false, { index: -1, count: 1 }); - expect(document.querySelector('.diagram-error-text')?.textContent).toBe('1 state error found'); - expect(button('state-error-show-btn').textContent).toBe('Show error'); + expect(button('diagram-focus-btn').closest('.diagram-error-legend')).not.toBeNull(); + expect(document.querySelector('.diagram-error-actions #diagram-focus-btn')).toBeNull(); }); - it('shows no state error badge or hint when the file has no state errors', () => { + it('shows no state error badge or summary when the file has no state errors', () => { renderStateMachineView(document.body, machine(), diagram, 'TB', false, false, { index: -1, count: 0 }); expect(document.querySelector('.nav-badge')).toBeNull(); diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index db190ba..ffe0836 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -6,15 +6,14 @@ import { renderMainHeader } from "../sections"; /** * The position of the shown state error among the state errors of the current file - * The index is -1 when none of them is shown + * The index is -1 when the shown error is from another file */ export type StateErrorNavigation = { index: number; count: number; }; -// shows the error context of the machine, if any, without stepping through errors -const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: 0, count: 0 }; +const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 }; export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError = false, stateErrors = NO_STATE_ERROR_NAVIGATION) { const previousDiagramContainer = root.querySelector('.diagram-container') as HTMLElement | null; @@ -23,8 +22,7 @@ export function renderStateMachineView(root: HTMLElement, sm: LJStateMachine | u } function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string { - const errorFocus = stateErrors.index >= 0 ? getStateErrorFocus(sm) : null; - const hiddenErrors = stateErrors.index < 0 ? renderHiddenStateErrors(stateErrors.count) : ''; + const errorFocus = getStateErrorFocus(sm); const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.toCondition) || sm.transitions.some(transition => !!transition.fromCondition || !!transition.toCondition) @@ -36,7 +34,6 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
    ${renderMainHeader("", 'fsm', stateErrors.count)} - ${!sm ? hiddenErrors : ''} ${sm ? /*html*/`
    @@ -51,7 +48,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
    - ${errorFocus ? renderStateErrorSummary(errorFocus, focusOnError, stateErrors) + renderStateErrorLegend(errorFocus) : hiddenErrors} + ${errorFocus ? renderStateErrorSummary(errorFocus, stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) : ''} ${showConditions && hasConditionExpansions ? /*html*/`
    Precondition @@ -65,12 +62,12 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
    ` - : hiddenErrors ? '' : 'No state machine available for the current file'} + : 'No state machine available for the current file'} `; } -function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean, stateErrors: StateErrorNavigation): string { +function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateErrorNavigation): string { const call = getRejectedCallText(focus); const receiver = focus.receiver ? `${escapeHtml(focus.receiver)}` : 'the receiver'; const rejected = `${call ? `${escapeHtml(call)}` : 'The call'} is rejected`; @@ -88,11 +85,8 @@ function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean,

    ${summary}

    - ${stateErrors.count > 1 ? renderStateErrorStepper(stateErrors) : ''} + ${stateErrors.index >= 0 && stateErrors.count > 1 ? renderStateErrorStepper(stateErrors) : ''} -
    `; @@ -108,19 +102,8 @@ function renderStateErrorStepper({ index, count }: StateErrorNavigation): string `; } -// points to the state errors of the current file when none of them is shown -function renderHiddenStateErrors(count: number): string { - if (count === 0) return ''; - return /*html*/` -
    -

    ${count} state error${count === 1 ? '' : 's'} found

    - -
    - `; -} - -// explains the state marks with the same outlines, fills, and icons as the diagram -function renderStateErrorLegend(focus: StateErrorFocus): string { +// explains the state marks with the same outlines, fills, and icons as the diagram, next to the toggle that dims the rest +function renderStateErrorLegend(focus: StateErrorFocus, focusOnError: boolean): string { const items = [ focus.invalidStates.length > 0 ? renderLegendItem('invalid', `${INVALID_STATE_ICON} Call rejected`) : '', focus.validStates.length > 0 ? renderLegendItem('valid', `${VALID_STATE_ICON} Call allowed`) : '', @@ -128,8 +111,14 @@ function renderStateErrorLegend(focus: StateErrorFocus): string { ? renderLegendItem('accepted', 'Allowed, but not reachable here') : '', ].filter(Boolean); - if (items.length === 0) return ''; - return `
    ${items.join('')}
    `; + return /*html*/` +
    + ${items.join('')} + +
    + `; } function renderLegendItem(kind: string, label: string): string { From 9fc9be9f6e2bed554aaea7b4ce117bedf9d837d4 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 21:27:22 +0000 Subject: [PATCH 3/3] Use the verifier's error context in the state error test fixtures Co-Authored-By: Claude Opus 5.5 --- client/src/webview/state-errors.spec.ts | 2 +- client/src/webview/views/fsm/fsm.spec.ts | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/client/src/webview/state-errors.spec.ts b/client/src/webview/state-errors.spec.ts index 567baf6..0c7c41f 100644 --- a/client/src/webview/state-errors.spec.ts +++ b/client/src/webview/state-errors.spec.ts @@ -12,7 +12,7 @@ function machine(className = 'javax.swing.tree.DefaultMutableTreeNode'): LJState className, states: ['childrenAllowed', 'maybeHasChildren'], initialTransitions: [{ to: 'childrenAllowed' }], transitions: [{ from: 'childrenAllowed', to: 'maybeHasChildren', label: 'add' }], - errorContext: { calledMethod: 'getFirstChild', actualStates: ['childrenAllowed'] }, + errorContext: { calledMethod: 'getFirstChild', receiver: 'root', possibleStates: ['childrenAllowed'], acceptedStates: ['maybeHasChildren'], validStates: [], invalidStates: ['childrenAllowed'] }, }; } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index c3207b8..1bb4c4a 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -226,7 +226,7 @@ describe('state machine view', () => { it('steps through several state errors and links back to the shown one', () => { const errorMachine = machine({ - errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, }); const stepButtons = () => Array.from(document.querySelectorAll('.state-error-step-btn'), node => [node.getAttribute('aria-label'), node.disabled]); @@ -248,7 +248,7 @@ describe('state machine view', () => { it('shows an error chosen from another file without stepping through the errors of the file', () => { const errorMachine = machine({ - errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, }); renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: -1, count: 2 }); @@ -259,7 +259,7 @@ describe('state machine view', () => { it('keeps the focus toggle with the legend, apart from the error actions', () => { const errorMachine = machine({ - errorContext: { calledMethod: 'read', actualStates: ['Closed'], expectedStates: ['Open'], possibleStates: ['Closed'] }, + errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, }); renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 });