Keep the stepper and View error when a state error cannot be marked, and put State Machine next to Verification

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?
 

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"

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'));

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);

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);
     }

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: {

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" })}
                             </div>
                         </div>
-                        ${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*/`
                             <div class="diagram-condition-legend">
                                 <span class="diagram-condition-legend-pre">Precondition</span>
@@ -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 ? `<code>${escapeHtml(focus.receiver)}</code>` : 'the receiver';
     const rejected = `${call ? `<code>${escapeHtml(call)}</code>` : '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 `<code>${escapeHtml(call)}</code> 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*/`
         <div class="diagram-error-summary">
             <p class="diagram-error-text">${summary}</p>

client/src/webview/views/sections.ts

@@ -141,8 +141,8 @@ export function renderNav(selectedTab: NavTab, stateErrorCount = 0): string {
         <nav>
             <ul>
                 <li><button class="nav-tab ${selectedTab === 'diagnostics' ? 'selected' : ''}" data-tab="diagnostics">Verification</button></li>
-                <li><button class="nav-tab ${selectedTab === 'context' ? 'selected' : ''}" data-tab="context">Context</button></li>
                 <li><button class="nav-tab ${selectedTab === 'fsm' ? 'selected' : ''}" data-tab="fsm">State Machine${stateErrorBadge}</button></li>
+                <li><button class="nav-tab ${selectedTab === 'context' ? 'selected' : ''}" data-tab="context">Context</button></li>
             </ul>
         </nav>
     `;