diff --git a/client/README.md b/client/README.md index 7b359af..cbbc4df 100644 --- a/client/README.md +++ b/client/README.md @@ -40,7 +40,7 @@ A repository with LiquidJava examples is available at [liquidjava-examples](http ### Getting started in VS Code -The **Get Started with LiquidJava** walkthrough introduces LiquidJava and its interactive tutorial, includes copyable Maven/Gradle annotation dependencies, then explains verification and its status indicator, diagnostics, context, state machines, the Command Palette, and logs. It also links to the [interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/). It opens once on installation, following VS Code’s walkthrough preferences. You can dismiss it at any time and reopen it with **LiquidJava: Show Walkthrough** from the Command Palette or **LiquidJava: Show Commands**. VS Code saves its progress across workspaces. +The **Get Started with LiquidJava** walkthrough introduces LiquidJava and its interactive tutorial, includes copyable Maven/Gradle annotation dependencies, then explains verification and its status indicator, diagnostics, state machines, context, the Command Palette, and logs. It also links to the [interactive tutorial](https://liquid-java.github.io/liquidjava-interactive-tutorial/). It opens once on installation, following VS Code’s walkthrough preferences. You can dismiss it at any time and reopen it with **LiquidJava: Show Walkthrough** from the Command Palette or **LiquidJava: Show Commands**. VS Code saves its progress across workspaces. ### What are Liquid Types? diff --git a/client/package.json b/client/package.json index 03c22c5..85cd42e 100644 --- a/client/package.json +++ b/client/package.json @@ -227,22 +227,22 @@ ] }, { - "id": "context", - "title": "Inspect context", - "description": "The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.\nLocal variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.\nClick a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.\n[Open LiquidJava view](command:liquidjava.showView)", + "id": "stateMachine", + "title": "Explore state machines", + "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab 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/context.md" + "markdown": "media/walkthrough/state-machine.md" }, "completionEvents": [ "onStepSelected" ] }, { - "id": "stateMachine", - "title": "Explore state machines", - "description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab 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)", + "id": "context", + "title": "Inspect context", + "description": "The **Context** tab shows **Variables**, **Aliases**, and **Ghosts** after verification. Expand or collapse each section.\nLocal variables are filtered by the cursor: only declarations before it and in enclosing scopes appear. Select a range to inspect declarations that overlap it; global variables are also included.\nClick a variable to reveal its source. Variables relevant to a nearby error are highlighted alongside the failing refinement.\n[Open LiquidJava view](command:liquidjava.showView)", "media": { - "markdown": "media/walkthrough/state-machine.md" + "markdown": "media/walkthrough/context.md" }, "completionEvents": [ "onStepSelected" diff --git a/client/src/test/walkthrough.test.ts b/client/src/test/walkthrough.test.ts index 9270f5b..899fe14 100644 --- a/client/src/test/walkthrough.test.ts +++ b/client/src/test/walkthrough.test.ts @@ -25,7 +25,7 @@ suite('LiquidJava walkthrough', () => { assert.ok(walkthrough); assert.equal(walkthrough.title, 'Get Started with LiquidJava'); assert.deepEqual(walkthrough.steps.map((step: { id: string }) => step.id), - ['tutorial', 'annotations', 'verification', 'commands', 'diagnostics', 'context', 'stateMachine', 'logs']); + ['tutorial', 'annotations', 'verification', 'commands', 'diagnostics', 'stateMachine', 'context', 'logs']); assert.equal(walkthrough.steps[0].title, 'Learn LiquidJava'); const commands = await vscode.commands.getCommands(true); assert.ok(commands.includes('liquidjava.showWalkthrough')); diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts index bfe2ed1..9b814ef 100644 --- a/client/src/webview/script.spec.ts +++ b/client/src/webview/script.spec.ts @@ -127,6 +127,12 @@ describe('webview script', () => { receive({ type: 'status', status: diagnostics.some(d => d.category === 'error') ? 'failed' : 'passed' }); } + it('puts the State Machine tab next to Verification, which link to each other', () => { + showDiagnostics([]); + + expect(Array.from(root.querySelectorAll('.nav-tab'), tab => tab.getAttribute('data-tab'))).toEqual(['diagnostics', 'fsm', 'context']); + }); + it('posts ready and renders the initial loading view', () => { expect(postMessage.mock.calls).toEqual([[{ type: 'ready' }]]); expect(root.querySelector('h2')?.textContent).toBe('Verification Pending'); @@ -309,6 +315,23 @@ describe('webview script', () => { expect(root.querySelectorAll('.diagnostic-state-machine-btn')).toHaveLength(1); }); + it('steps through state errors the verifier could not mark on the diagram', () => { + showDiagnostics([ + stateError('First state error', { ...errorMachine('First', 'close'), errorContext: null }, 4), + stateError('Second state error', { ...errorMachine('Second', 'reset'), errorContext: null }, 9), + ]); + click('[data-tab="fsm"]'); + expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 5 is rejected'); + 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('.diagram-error-text')?.textContent).toBe('The call at line 10 is rejected'); + + click('#state-error-reveal-btn'); + expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics'); + }); + 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); diff --git a/client/src/webview/script.ts b/client/src/webview/script.ts index 6dcb6f5..672795e 100644 --- a/client/src/webview/script.ts +++ b/client/src/webview/script.ts @@ -430,7 +430,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) ? createMermaidDiagram({ ...displayedStateMachine, errorContext: null }, diagramOrientation, showDiagramConditions) : diagram; renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError, - { index: shownIndex, count: stateErrors.length }); + { index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) }); renderedStateMachineView = getStateMachineViewKey(); if (displayedStateMachine) renderMermaidDiagram(document, window); break; @@ -441,6 +441,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window) } } + // the 1-based line of the shown error, null without a position, undefined when no error is shown + function getStateErrorLine(error: StateRefinementError | undefined): number | null | undefined { + if (!error) return undefined; + return error.position ? error.position.lineStart + 1 : null; + } + function getCurrentStateErrors(): StateRefinementError[] { return getStateErrors(diagnostics, currentFile); } diff --git a/client/src/webview/views/fsm/fsm.spec.ts b/client/src/webview/views/fsm/fsm.spec.ts index 1bb4c4a..f28de28 100644 --- a/client/src/webview/views/fsm/fsm.spec.ts +++ b/client/src/webview/views/fsm/fsm.spec.ts @@ -196,6 +196,29 @@ describe('state machine view', () => { expect(document.querySelector('#diagram-focus-btn')).toBeNull(); }); + it.each([ + ['without the accepted states', { + calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'], + acceptedStates: [], validStates: [], invalidStates: [], + }, 'counter.open() is rejected here'], + ['without an error context', null, 'The call at line 12 is rejected'], + ])('keeps the stepper and View error for a shown error %s', (_, errorContext, text) => { + renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true, { index: 1, count: 2, line: 12 }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe(text); + expect(document.querySelector('.state-error-position')?.textContent).toBe('2 of 2'); + expect(button('state-error-reveal-btn')).not.toBeNull(); + // nothing is marked, so there is nothing to explain or dim + expect(document.querySelector('.diagram-error-legend')).toBeNull(); + expect(document.querySelector('#diagram-focus-btn')).toBeNull(); + }); + + it('says the call is rejected without a line when the shown error has no position', () => { + renderStateMachineView(document.body, machine(), diagram, 'TB', false, true, { index: -1, count: 0, line: null }); + + expect(document.querySelector('.diagram-error-text')?.textContent).toBe('The call is rejected'); + }); + it('clips the panned diagram below the error summary and legend', () => { renderStateMachineView(document.body, machine({ errorContext: { diff --git a/client/src/webview/views/fsm/fsm.ts b/client/src/webview/views/fsm/fsm.ts index ffe0836..88d9c8b 100644 --- a/client/src/webview/views/fsm/fsm.ts +++ b/client/src/webview/views/fsm/fsm.ts @@ -11,6 +11,8 @@ import { renderMainHeader } from "../sections"; export type StateErrorNavigation = { index: number; count: number; + // the 1-based line of the shown error, if any error is shown + line?: number | null; }; const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 }; @@ -48,7 +50,9 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str ${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })} - ${errorFocus ? renderStateErrorSummary(errorFocus, stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) : ''} + ${errorFocus + ? renderStateErrorSummary(getStateErrorSummary(errorFocus), stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) + : isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sm, stateErrors), stateErrors) : ''} ${showConditions && hasConditionExpansions ? /*html*/`
Precondition @@ -67,7 +71,11 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str `; } -function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateErrorNavigation): string { +function isStateErrorShown(stateErrors: StateErrorNavigation): boolean { + return stateErrors.index >= 0 || stateErrors.line !== undefined; +} + +function getStateErrorSummary(focus: StateErrorFocus): string { const call = getRejectedCallText(focus); const receiver = focus.receiver ? `${escapeHtml(focus.receiver)}` : 'the receiver'; const rejected = `${call ? `${escapeHtml(call)}` : 'The call'} is rejected`; @@ -81,6 +89,20 @@ function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateError summary = `${rejected} here`; } if (allowedStates.length > 0) summary += ` \u00B7 allowed in state ${renderStates(allowedStates)}`; + return summary; +} + +// the shown error cannot be marked on the diagram when the verifier could not tell which states allow the call +function getUnmarkedStateErrorSummary(sm: LJStateMachine, stateErrors: StateErrorNavigation): string { + const context = sm.errorContext; + if (context?.calledMethod) { + const call = `${context.receiver ? `${context.receiver}.` : ''}${context.calledMethod}()`; + return `${escapeHtml(call)} is rejected here`; + } + return stateErrors.line ? `The call at line ${stateErrors.line} is rejected` : 'The call is rejected'; +} + +function renderStateErrorSummary(summary: string, stateErrors: StateErrorNavigation): string { return /*html*/`

${summary}

diff --git a/client/src/webview/views/sections.ts b/client/src/webview/views/sections.ts index de512f5..3dd7b6d 100644 --- a/client/src/webview/views/sections.ts +++ b/client/src/webview/views/sections.ts @@ -141,8 +141,8 @@ export function renderNav(selectedTab: NavTab, stateErrorCount = 0): string { `;