From 31edcee58ce21e6487000825f8271018bc13def2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 24 Oct 2026 23:45:58 +0100 Subject: [PATCH] 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 d643e31..234bfdd 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 ad639c8..7c2d87c 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -216,4 +216,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(); +}