Open the State Machine view on the first state error of the file

Count only the state errors of the current file, keep the focus toggle with
the legend apart from View error, and move Show in state machine to the top
of the error.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

client/media/walkthrough/state-machine.md

@@ -1,4 +1,4 @@
 The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`.
 Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.
 Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.
-From a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.
+From a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.

client/package.json

@@ -240,7 +240,7 @@
 					{
 						"id": "stateMachine",
 						"title": "Explore state machines",
-						"description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab keeps the last state error shown and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)",
+						"description": "The **State Machine** tab shows object states and method transitions declared with ``@StateSet`` and ``@StateRefinement``.\nPan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.\nUse **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.\nFrom a state error, choose **Show in state machine** to see the related states and call. The tab opens on the first state error of the file, keeps the one you choose, and follows the error at the cursor; step through several with the arrows, and use **View error** to go back to it.\n[Open LiquidJava view](command:liquidjava.showView)",
 						"media": {
 							"markdown": "media/walkthrough/state-machine.md"
 						},

client/src/webview/script.spec.ts

@@ -57,10 +57,10 @@ const stateMachine: LJStateMachine = {
     errorContext: null,
 };
 
-function stateError(title: string, sm: LJStateMachine, line = position.lineStart): LJDiagnostic {
-    const errorPosition = { ...position, lineStart: line, lineEnd: line };
+function stateError(title: string, sm: LJStateMachine, line = position.lineStart, file = currentFile): LJDiagnostic {
+    const errorPosition = { ...position, file, lineStart: line, lineEnd: line };
     return {
-        title, message: `${title} message`, hint: null, file: currentFile, position: errorPosition,
+        title, message: `${title} message`, hint: null, file, position: errorPosition,
         category: 'error', type: 'state-refinement-error', translationTable: {}, expected: 'Open(counter)',
         found: { implication: null as never, origin: null, simplification: 'Closed(counter)' },
         customMessage: '', declarationPosition: null, stateMachine: sm,
@@ -285,16 +285,28 @@ describe('webview script', () => {
         expect(root.querySelector('.diagram-title')?.textContent).toBe('First');
     });
 
-    it('points to the state errors of the file until one is shown', () => {
-        showDiagnostics([stateError('State refinement error', errorMachine('Counter', 'close'))]);
+    it('opens on the first state error of the file, focused', () => {
+        showDiagnostics([
+            stateError('Second state error', errorMachine('Second', 'reset'), 9),
+            stateError('First state error', errorMachine('First', 'close'), 4),
+        ]);
         receive({ type: 'fsm', sm: stateMachine });
         click('[data-tab="fsm"]');
-        expect(root.querySelector('.diagram-error-text')?.textContent).toBe('1 state error found');
-        expect(root.querySelector('.mermaid')?.textContent).not.toContain('ljState');
 
-        click('#state-error-show-btn');
+        expect(root.querySelector('.diagram-title')?.textContent).toBe('First');
+        expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2');
         expect(root.querySelector('#diagram-focus-btn')?.textContent?.trim()).toBe('Show all');
-        expect(root.querySelector('.mermaid')?.textContent).toContain('class Broken ljStateDimmed');
+        expect(root.querySelector('.mermaid')?.textContent).toContain('ljStateDimmed');
+    });
+
+    it('counts only the state errors of the current file, as listed in the Verification tab', () => {
+        showDiagnostics([
+            stateError('State refinement error', errorMachine('Counter', 'close'), 4),
+            stateError('Other file error', errorMachine('Counter', 'close'), 2, otherFile),
+        ]);
+
+        expect(root.querySelector('[data-tab="fsm"] .nav-badge')?.textContent).toBe('1');
+        expect(root.querySelectorAll('.diagnostic-state-machine-btn')).toHaveLength(1);
     });
 
     it('follows the state error at the cursor without overriding a later choice', () => {
@@ -368,6 +380,21 @@ describe('webview script', () => {
 
         expect(root.querySelector('.diagnostic-state-machine-btn')?.textContent?.trim()).toBe('Show in state machine');
         expect(root.querySelector('.diagnostic-actions .diagnostic-state-machine-btn')).toBeNull();
+        // right below the error message, before its details
+        const firstSection = root.querySelector('.error-item .section')!;
+        expect(root.querySelector('.diagnostic-state-machine-btn')!.compareDocumentPosition(firstSection)).toBe(Node.DOCUMENT_POSITION_FOLLOWING);
+    });
+
+    it('opens on the first state error of a newly opened file', () => {
+        showDiagnostics([
+            stateError('Main error', errorMachine('Main', 'close'), 4),
+            stateError('Other file error', errorMachine('Other', 'close'), 2, otherFile),
+        ]);
+        click('.diagnostic-state-machine-btn');
+        expect(root.querySelector('.diagram-title')?.textContent).toBe('Main');
+
+        receive({ type: 'file', file: otherFile });
+        expect(root.querySelector('.diagram-title')?.textContent).toBe('Other');
     });
 
     it('toggles between file and workspace errors by clicking scope buttons', () => {

client/src/webview/script.ts

@@ -41,7 +41,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     let status: ExtensionStatus = 'loading';
     let diagramOrientation: "LR" | "TB" = "TB";
     let showDiagramConditions = false;
-    let focusDiagramOnError = false;
+    let focusDiagramOnError = true;
     let currentDiagram: string = '';
     let renderedStateMachineView: string | undefined;
     let revealTimeout: ReturnType<typeof setTimeout> | undefined;
@@ -156,23 +156,16 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             e.stopPropagation();
             if ((stateErrorStepButton as HTMLButtonElement).disabled) return;
             const errors = getCurrentStateErrors();
-            const index = getShownStateErrorIndex(errors) + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10);
+            const index = getShownStateError(errors).index + parseInt(stateErrorStepButton.getAttribute('data-step') || '0', 10);
             if (errors[index]) showStateError(errors[index]);
             return;
         }
 
-        // show the first state error of the current file
-        if (target.closest?.('#state-error-show-btn')) {
-            e.stopPropagation();
-            const [first] = getCurrentStateErrors();
-            if (first) showStateError(first);
-            return;
-        }
-
         // go back to the shown state error in the Verification tab
         if (target.closest?.('#state-error-reveal-btn')) {
             e.stopPropagation();
-            const revealTarget = selectedStateError && getDiagnosticRevealTarget(selectedStateError);
+            const { error } = getShownStateError(getCurrentStateErrors());
+            const revealTarget = error && getDiagnosticRevealTarget(error);
             if (revealTarget) revealDiagnostic(revealTarget);
             return;
         }
@@ -378,6 +371,8 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
             }
             case 'file':
                 currentFile = msg.file;
+                // the view shows the first error of the new file instead
+                if (selectedStateError && selectedStateError.file.toLowerCase() !== currentFile?.toLowerCase()) selectedStateError = undefined;
                 if (diagnostics && !showAllDiagnostics && selectedTab === 'diagnostics') updateView();
                 stateMachine = undefined;
                 if (selectedTab === 'fsm') updateStateMachineViewIfChanged();
@@ -426,8 +421,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
                     : renderLoading();
                 break;
             case 'fsm': {
-                const shownIndex = getShownStateErrorIndex(stateErrors);
-                const shownError = stateErrors[shownIndex];
+                const { error: shownError, index: shownIndex } = getShownStateError(stateErrors);
                 const displayedStateMachine = shownError?.stateMachine ?? stateMachine;
                 const focusOnError = focusDiagramOnError && !!shownError;
                 const diagram = createMermaidDiagram(displayedStateMachine, diagramOrientation, showDiagramConditions, focusOnError);
@@ -448,13 +442,17 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
     }
 
     function getCurrentStateErrors(): StateRefinementError[] {
-        return getStateErrors(diagnostics, currentFile, stateMachine);
+        return getStateErrors(diagnostics, currentFile);
     }
 
-    function getShownStateErrorIndex(errors: StateRefinementError[]): number {
-        if (!selectedStateError) return -1;
+    /**
+     * Gets the state error the view shows and its index among the state errors of the current file
+     * This is the selected error, which is outside them when chosen from another file, or else the first one
+     */
+    function getShownStateError(errors: StateRefinementError[]): { error: StateRefinementError | undefined; index: number } {
+        if (!selectedStateError) return { error: errors[0], index: errors.length > 0 ? 0 : -1 };
         const key = getStateErrorKey(selectedStateError);
-        return errors.findIndex(error => getStateErrorKey(error) === key);
+        return { error: selectedStateError, index: errors.findIndex(error => getStateErrorKey(error) === key) };
     }
 
     function findStateErrorAt(target: DiagnosticRevealTarget): StateRefinementError | undefined {
@@ -497,7 +495,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
 
     function getStateMachineViewKey(): string {
         const stateErrors = getCurrentStateErrors();
-        const shownError = stateErrors[getShownStateErrorIndex(stateErrors)];
+        const { error: shownError } = getShownStateError(stateErrors);
         return JSON.stringify([shownError?.stateMachine ?? stateMachine ?? null, shownError ? getStateErrorKey(shownError) : null, stateErrors.length]);
     }
 

client/src/webview/state-errors.spec.ts

@@ -44,20 +44,11 @@ describe('state errors', () => {
     it('lists the errors of the current file in source order', () => {
         const later = stateError(20);
         const earlier = stateError(10);
-        const otherFile = stateError(5, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') });
+        const otherFile = stateError(5, { file: otherCallerFile });
 
-        expect(getStateErrors([later, otherFile, earlier], callerFile, undefined)).toEqual([earlier, later]);
-        expect(getStateErrors([later], undefined, undefined)).toEqual([]);
-    });
-
-    it('adds the errors on the state machine of the current file from other files after its own', () => {
-        const ownError = stateError(30, { file: refinementsFile, stateMachine: machine('java.util.ArrayList') });
-        const callerError = stateError(10);
-        const otherCallerError = stateError(4, { file: otherCallerFile });
-        const otherMachine = stateError(2, { file: otherCallerFile, stateMachine: machine('java.util.ArrayList') });
-
-        expect(getStateErrors([callerError, otherMachine, otherCallerError, ownError], refinementsFile, machine()))
-            .toEqual([ownError, otherCallerError, callerError]);
+        expect(getStateErrors([later, otherFile, earlier], callerFile)).toEqual([earlier, later]);
+        expect(getStateErrors([later, otherFile], refinementsFile)).toEqual([]);
+        expect(getStateErrors([later], undefined)).toEqual([]);
     });
 
     it('finds the selected error again after verification', () => {

client/src/webview/state-errors.ts

@@ -1,23 +1,18 @@
 import type { LJDiagnostic, StateRefinementError } from "../types/diagnostics";
-import type { LJStateMachine } from "../types/fsm";
 import { getDiagnosticRevealTarget, getDiagnosticRevealTargetKey } from "./diagnostic-reveal";
 
 /**
- * Gets the state errors that the State Machine view can show for the current file
- * These are the state errors reported in the file and, since errors are usually reported in the caller file,
- * the ones on the state machine declared in the file, with the errors of the file first in source order
+ * Gets the state errors reported in the current file, in source order
+ * These are the errors the State Machine view steps through, one for each Show in state machine button of the file
  * @param diagnostics All diagnostics in the workspace
  * @param currentFile The file open in the editor
- * @param sm The state machine declared in the current file
  */
-export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined, sm: LJStateMachine | undefined): StateRefinementError[] {
-    const isCurrentFile = (error: StateRefinementError) => !!currentFile && error.file.toLowerCase() === currentFile.toLowerCase();
+export function getStateErrors(diagnostics: LJDiagnostic[] | undefined, currentFile: string | undefined): StateRefinementError[] {
+    if (!currentFile) return [];
     return getAllStateErrors(diagnostics)
-        .filter(error => isCurrentFile(error) || error.stateMachine?.className === sm?.className)
+        .filter(error => error.file.toLowerCase() === currentFile.toLowerCase())
         .map((error, index) => ({ error, index }))
-        .sort((a, b) => Number(isCurrentFile(b.error)) - Number(isCurrentFile(a.error))
-            || a.error.file.localeCompare(b.error.file)
-            || (a.error.position?.lineStart ?? 0) - (b.error.position?.lineStart ?? 0)
+        .sort((a, b) => (a.error.position?.lineStart ?? 0) - (b.error.position?.lineStart ?? 0)
             || (a.error.position?.colStart ?? 0) - (b.error.position?.colStart ?? 0)
             || a.index - b.index)
         .map(({ error }) => error);

client/src/webview/styles.ts

@@ -252,7 +252,7 @@ export function getStyles(): string {
             display: inline-flex;
             align-items: center;
             gap: 0.4rem;
-            margin: 0.75rem 0 0.25rem;
+            margin: 0 0 1rem;
             padding: 0.25rem 0.6rem;
             color: var(--vscode-button-secondaryForeground);
             background-color: var(--vscode-button-secondaryBackground);
@@ -1095,6 +1095,7 @@ export function getStyles(): string {
         }
         .diagram-focus-btn {
             flex-shrink: 0;
+            margin-left: auto;
         }
         .diagram-error-actions {
             display: flex;
@@ -1124,6 +1125,7 @@ export function getStyles(): string {
         .diagram-error-legend {
             display: flex;
             flex-wrap: wrap;
+            align-items: center;
             gap: 0.25rem 1rem;
             margin-bottom: 0.75rem;
             font-size: 0.8rem;

client/src/webview/views/diagnostics/errors.ts

@@ -25,8 +25,7 @@ export function renderErrors(errors: LJError[]): string {
                         ${renderDiagnosticContextAction(error)}
                         ${renderCopyDiagnosticButton('error', index)}
                     </div>
-                    ${renderError(error)}
-                    ${renderDiagnosticStateMachineAction(error, index)}
+                    ${renderError(error, renderDiagnosticStateMachineAction(error, index))}
                 </li>
             `;
             }).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 {