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..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 **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 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 814ca37..03c22c5 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 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/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..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, @@ -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,139 @@ 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('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-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('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', () => { + 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(); + // 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', () => { showDiagnostics([ diagnostic(currentFile, 'Current error'), diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 3fe2fa8..6dcb6f5 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,16 +32,18 @@ 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'; 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; const contextSectionState: ContextSectionState = { aliases: false, @@ -143,15 +146,27 @@ 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 = getShownStateError(errors).index + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10); + if (errors[index]) showStateError(errors[index]); + return; + } + + // go back to the shown state error in the Verification tab + if (target.closest?.('#state-error-reveal-btn')) { + e.stopPropagation(); + const { error } = getShownStateError(getCurrentStateErrors()); + const revealTarget = error && getDiagnosticRevealTarget(error); + if (revealTarget) revealDiagnostic(revealTarget); return; } @@ -281,10 +296,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 +362,38 @@ 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; + // 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(); - 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 +412,93 @@ 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 { error: shownError, index: shownIndex } = getShownStateError(stateErrors); + 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); + } + + /** + * 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 { error: selectedStateError, index: 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 { error: shownError } = getShownStateError(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..0c7c41f --- /dev/null +++ b/client/src/webview/state-errors.spec.ts @@ -0,0 +1,83 @@ +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', receiver: 'root', possibleStates: ['childrenAllowed'], acceptedStates: ['maybeHasChildren'], validStates: [], invalidStates: ['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 }); + + 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', () => { + 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..88e7a19 --- /dev/null +++ b/client/src/webview/state-errors.ts @@ -0,0 +1,63 @@ +import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics"; +import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal"; + +/** + * 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 + */ +export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined): StateRefinementError[] { + if (!currentFile) return []; + return getAllStateErrors(diagnostics) + .filter(error => error.file.toLowerCase() === currentFile.toLowerCase()) + .map((error, index) => ({ error, index })) + .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); +} + +/** + * 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..abef3e0 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 0 1rem; + 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; } @@ -1071,10 +1095,37 @@ export function getStyles(): string { } .diagram-focus-btn { flex-shrink: 0; + margin-left: auto; + } + .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; + align-items: center; gap: 0.25rem 1rem; margin-bottom: 0.75rem; font-size: 0.8rem; 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..1b9db34 100644 --- a/client/src/webview/views/diagnostics/errors.ts +++ b/client/src/webview/views/diagnostics/errors.ts @@ -22,11 +22,10 @@ export function renderErrors(errors: LJError[]): string { return /*html*/`
  • - ${renderDiagnosticStateMachineAction(error, index)} ${renderDiagnosticContextAction(error)} ${renderCopyDiagnosticButton('error', index)}
    - ${renderError(error)} + ${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 f17d6e5..1bb4c4a 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -223,4 +223,54 @@ 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', 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]); + + 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('shows an error chosen from another file without stepping through the errors of the file', () => { + const errorMachine = machine({ + errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, + }); + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: -1, count: 2 }); + + expect(document.querySelector('.state-error-stepper')).toBeNull(); + expect(button('state-error-reveal-btn')).not.toBeNull(); + expect(document.querySelector('.nav-badge')?.textContent).toBe('2'); + }); + + it('keeps the focus toggle with the legend, apart from the error actions', () => { + const errorMachine = machine({ + errorContext: { calledMethod: 'read', receiver: 'connection', possibleStates: ['Closed'], acceptedStates: ['Open'], validStates: [], invalidStates: ['Closed'] }, + }); + renderStateMachineView(document.body, errorMachine, diagram, 'TB', false, true, { index: 0, count: 3 }); + + 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 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(); + 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..ffe0836 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -4,13 +4,24 @@ 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 the shown error is from another file + */ +export type StateErrorNavigation = { + index: number; + count: number; +}; + +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; 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 { +function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: string, orientation: "LR" | "TB", showConditions: boolean, focusOnError: boolean, stateErrors: StateErrorNavigation, diagramHeight?: number): string { const errorFocus = getStateErrorFocus(sm); const hasConditionExpansions = sm ? sm.initialTransitions.some(transition => !!transition.toCondition) @@ -22,7 +33,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str return /*html*/`
    - ${renderMainHeader("", 'fsm')} + ${renderMainHeader("", 'fsm', stateErrors.count)} ${sm ? /*html*/`
    @@ -37,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) + renderStateErrorLegend(errorFocus) : ''} + ${errorFocus ? renderStateErrorSummary(errorFocus, stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) : ''} ${showConditions && hasConditionExpansions ? /*html*/`
    Precondition @@ -56,7 +67,7 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str `; } -function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean): 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`; @@ -73,15 +84,26 @@ function renderStateErrorSummary(focus: StateErrorFocus, focusOnError: boolean): return /*html*/`

    ${summary}

    - +
    + ${stateErrors.index >= 0 && stateErrors.count > 1 ? renderStateErrorStepper(stateErrors) : ''} + +
    `; } -// explains the state marks with the same outlines, fills, and icons as the diagram -function renderStateErrorLegend(focus: StateErrorFocus): string { +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 })} + + `; +} + +// 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`) : '', @@ -89,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 { 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(); +}