Skip to content

Commit 67a862b

Browse files
Keep the stepper and View error when a state error cannot be marked
When the verifier cannot tell which states allow the call, the diagram has no marks and the error summary was not shown, so the state errors could not be stepped through or opened in the Verification tab. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 9fc9be9 commit 67a862b

4 files changed

Lines changed: 71 additions & 3 deletions

File tree

‎client/src/webview/script.spec.ts‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -309,6 +309,23 @@ describe('webview script', () => {
309309
expect(root.querySelectorAll('.diagnostic-state-machine-btn')).toHaveLength(1);
310310
});
311311

312+
it('steps through state errors the verifier could not mark on the diagram', () => {
313+
showDiagnostics([
314+
stateError('First state error', { ...errorMachine('First', 'close'), errorContext: null }, 4),
315+
stateError('Second state error', { ...errorMachine('Second', 'reset'), errorContext: null }, 9),
316+
]);
317+
click('[data-tab="fsm"]');
318+
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 5 is rejected');
319+
expect(root.querySelector('.state-error-position')?.textContent).toBe('1 of 2');
320+
321+
click('.state-error-step-btn[data-step="1"]');
322+
expect(root.querySelector('.diagram-title')?.textContent).toBe('Second');
323+
expect(root.querySelector('.diagram-error-text')?.textContent).toBe('The call at line 10 is rejected');
324+
325+
click('#state-error-reveal-btn');
326+
expect(root.querySelector('.nav-tab.selected')?.getAttribute('data-tab')).toBe('diagnostics');
327+
});
328+
312329
it('follows the state error at the cursor without overriding a later choice', () => {
313330
const first = stateError('First state error', errorMachine('First', 'close'), 4);
314331
const second = stateError('Second state error', errorMachine('Second', 'reset'), 9);

‎client/src/webview/script.ts‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -430,7 +430,7 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
430430
? createMermaidDiagram({ ...displayedStateMachine, errorContext: null }, diagramOrientation, showDiagramConditions)
431431
: diagram;
432432
renderStateMachineView(root, displayedStateMachine, diagram, diagramOrientation, showDiagramConditions, focusOnError,
433-
{ index: shownIndex, count: stateErrors.length });
433+
{ index: shownIndex, count: stateErrors.length, line: getStateErrorLine(shownError) });
434434
renderedStateMachineView = getStateMachineViewKey();
435435
if (displayedStateMachine) renderMermaidDiagram(document, window);
436436
break;
@@ -441,6 +441,12 @@ export function getScript(vscode: VSCodeApi, document: Document, window: Window)
441441
}
442442
}
443443

444+
// the 1-based line of the shown error, null without a position, undefined when no error is shown
445+
function getStateErrorLine(error: StateRefinementError | undefined): number | null | undefined {
446+
if (!error) return undefined;
447+
return error.position ? error.position.lineStart + 1 : null;
448+
}
449+
444450
function getCurrentStateErrors(): StateRefinementError[] {
445451
return getStateErrors(diagnostics, currentFile);
446452
}

‎client/src/webview/views/fsm/fsm.spec.ts‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -196,6 +196,29 @@ describe('state machine view', () => {
196196
expect(document.querySelector('#diagram-focus-btn')).toBeNull();
197197
});
198198

199+
it.each([
200+
['without the accepted states', {
201+
calledMethod: 'open', receiver: 'counter', possibleStates: ['Closed'],
202+
acceptedStates: [], validStates: [], invalidStates: [],
203+
}, 'counter.open() is rejected here'],
204+
['without an error context', null, 'The call at line 12 is rejected'],
205+
])('keeps the stepper and View error for a shown error %s', (_, errorContext, text) => {
206+
renderStateMachineView(document.body, machine({ errorContext }), diagram, 'TB', false, true, { index: 1, count: 2, line: 12 });
207+
208+
expect(document.querySelector('.diagram-error-text')?.textContent).toBe(text);
209+
expect(document.querySelector('.state-error-position')?.textContent).toBe('2 of 2');
210+
expect(button('state-error-reveal-btn')).not.toBeNull();
211+
// nothing is marked, so there is nothing to explain or dim
212+
expect(document.querySelector('.diagram-error-legend')).toBeNull();
213+
expect(document.querySelector('#diagram-focus-btn')).toBeNull();
214+
});
215+
216+
it('says the call is rejected without a line when the shown error has no position', () => {
217+
renderStateMachineView(document.body, machine(), diagram, 'TB', false, true, { index: -1, count: 0, line: null });
218+
219+
expect(document.querySelector('.diagram-error-text')?.textContent).toBe('The call is rejected');
220+
});
221+
199222
it('clips the panned diagram below the error summary and legend', () => {
200223
renderStateMachineView(document.body, machine({
201224
errorContext: {

‎client/src/webview/views/fsm/fsm.ts‎

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@ import { renderMainHeader } from "../sections";
1111
export type StateErrorNavigation = {
1212
index: number;
1313
count: number;
14+
// the 1-based line of the shown error, if any error is shown
15+
line?: number | null;
1416
};
1517

1618
const NO_STATE_ERROR_NAVIGATION: StateErrorNavigation = { index: -1, count: 0 };
@@ -48,7 +50,9 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
4850
${renderCodiconButton("copy", { id: "copy-diagram-btn", className: "diagram-control-btn", title: "Copy Mermaid Source" })}
4951
</div>
5052
</div>
51-
${errorFocus ? renderStateErrorSummary(errorFocus, stateErrors) + renderStateErrorLegend(errorFocus, focusOnError) : ''}
53+
${errorFocus
54+
? renderStateErrorSummary(getStateErrorSummary(errorFocus), stateErrors) + renderStateErrorLegend(errorFocus, focusOnError)
55+
: isStateErrorShown(stateErrors) ? renderStateErrorSummary(getUnmarkedStateErrorSummary(sm, stateErrors), stateErrors) : ''}
5256
${showConditions && hasConditionExpansions ? /*html*/`
5357
<div class="diagram-condition-legend">
5458
<span class="diagram-condition-legend-pre">Precondition</span>
@@ -67,7 +71,11 @@ function renderStateMachineViewHtml(sm: LJStateMachine | undefined, diagram: str
6771
`;
6872
}
6973

70-
function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateErrorNavigation): string {
74+
function isStateErrorShown(stateErrors: StateErrorNavigation): boolean {
75+
return stateErrors.index >= 0 || stateErrors.line !== undefined;
76+
}
77+
78+
function getStateErrorSummary(focus: StateErrorFocus): string {
7179
const call = getRejectedCallText(focus);
7280
const receiver = focus.receiver ? `<code>${escapeHtml(focus.receiver)}</code>` : 'the receiver';
7381
const rejected = `${call ? `<code>${escapeHtml(call)}</code>` : 'The call'} is rejected`;
@@ -81,6 +89,20 @@ function renderStateErrorSummary(focus: StateErrorFocus, stateErrors: StateError
8189
summary = `${rejected} here`;
8290
}
8391
if (allowedStates.length > 0) summary += ` \u00B7 allowed in state ${renderStates(allowedStates)}`;
92+
return summary;
93+
}
94+
95+
// the shown error cannot be marked on the diagram when the verifier could not tell which states allow the call
96+
function getUnmarkedStateErrorSummary(sm: LJStateMachine, stateErrors: StateErrorNavigation): string {
97+
const context = sm.errorContext;
98+
if (context?.calledMethod) {
99+
const call = `${context.receiver ? `${context.receiver}.` : ''}${context.calledMethod}()`;
100+
return `<code>${escapeHtml(call)}</code> is rejected here`;
101+
}
102+
return stateErrors.line ? `The call at line ${stateErrors.line} is rejected` : 'The call is rejected';
103+
}
104+
105+
function renderStateErrorSummary(summary: string, stateErrors: StateErrorNavigation): string {
84106
return /*html*/`
85107
<div class="diagram-error-summary">
86108
<p class="diagram-error-text">${summary}</p>

0 commit comments

Comments
 (0)