Skip to content

Commit 79accc2

Browse files
Keep the state error in the State Machine view and link it to the editor
The tab keeps the last state error shown and follows the error at the cursor, steps through several errors, counts them on the tab, and links back to the error in the Verification tab. State errors get a labelled Show in state machine button and CodeLens. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent f1c258a commit 79accc2

19 files changed

Lines changed: 694 additions & 89 deletions

File tree

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
The **Verification** tab compares **Found** with **Expected**. Click a location or variable to jump to its source.
22
When a simplification history is available, use **Previous simplification** and **Next simplification** to inspect highlighted changes. Inspect a **Hint** or **Counterexample** when available.
3-
Switch between **Current file** and **Workspace**, or use **View related context** and **View error on state machine** to investigate an error.
3+
Switch between **Current file** and **Workspace**, or use **View related context** and **Show in state machine** to investigate an error.
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
The **State Machine** tab shows object states and method transitions declared with `@StateSet` and `@StateRefinement`.
22
Pan the diagram; use **Zoom In**, **Zoom Out**, **Reset Zoom**, and **Toggle Orientation** to inspect it.
33
Use **Expand Conditions** or **Collapse Conditions** to show or hide preconditions and postconditions. **Copy Mermaid Source** copies the diagram definition.
4-
From a state error, choose **View error on state machine** to see the related states and call.
4+
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.

‎client/package.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@
218218
{
219219
"id": "diagnostics",
220220
"title": "Understand diagnostics",
221-
"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)",
221+
"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)",
222222
"media": {
223223
"markdown": "media/walkthrough/diagnostics.md"
224224
},
@@ -240,7 +240,7 @@
240240
{
241241
"id": "stateMachine",
242242
"title": "Explore state machines",
243-
"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)",
243+
"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)",
244244
"media": {
245245
"markdown": "media/walkthrough/state-machine.md"
246246
},

‎client/src/services/codelens.ts‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,7 @@ export function registerCodeLens(context: vscode.ExtensionContext) {
1616

1717
const file = normalizeFilePath(document.uri.fsPath);
1818
return (extension.diagnostics || [])
19-
.map(diagnostic => createDiagnosticCodeLens(diagnostic, file))
20-
.filter((codeLens): codeLens is vscode.CodeLens => Boolean(codeLens));
19+
.flatMap(diagnostic => createDiagnosticCodeLenses(diagnostic, file));
2120
}
2221
})
2322
);
@@ -27,18 +26,26 @@ export function refreshCodeLenses() {
2726
codeLensEmitter.fire();
2827
}
2928

30-
function createDiagnosticCodeLens(diagnostic: LJDiagnostic, file: string): vscode.CodeLens | undefined {
29+
function createDiagnosticCodeLenses(diagnostic: LJDiagnostic, file: string): vscode.CodeLens[] {
3130
const targetDiagnostic = getDiagnosticRevealTarget(diagnostic);
32-
if (!targetDiagnostic || targetDiagnostic.file !== file) return undefined;
31+
if (!targetDiagnostic || targetDiagnostic.file !== file) return [];
3332

3433
const position = targetDiagnostic.position;
3534
const range = new vscode.Range(
3635
new vscode.Position(position.lineStart, position.colStart),
3736
new vscode.Position(position.lineStart, position.colStart)
3837
);
39-
return new vscode.CodeLens(range, {
38+
const codeLenses = [new vscode.CodeLens(range, {
4039
title: diagnostic.title,
4140
command: "liquidjava.showView",
4241
arguments: [targetDiagnostic]
43-
});
42+
})];
43+
if (diagnostic.type === 'state-refinement-error' && diagnostic.stateMachine) {
44+
codeLenses.push(new vscode.CodeLens(range, {
45+
title: "Show in state machine",
46+
command: "liquidjava.showView",
47+
arguments: [targetDiagnostic, 'fsm']
48+
}));
49+
}
50+
return codeLenses;
4451
}

‎client/src/services/webview.ts‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,15 @@ import * as vscode from "vscode";
22
import { LiquidJavaWebviewProvider } from "../webview/provider";
33
import { extension } from "../state";
44
import type { DiagnosticRevealTarget } from "../types/diagnostics";
5+
import type { NavTab } from "../webview/views/sections";
56

67
/**
78
* Initializes the webview panel for the extension
89
* @param context The extension context
910
*/
1011
export function registerWebview(context: vscode.ExtensionContext) {
1112
extension.webview = new LiquidJavaWebviewProvider(context.extensionUri);
12-
let pendingDiagnosticReveal: DiagnosticRevealTarget | undefined;
13+
let pendingDiagnosticReveal: { diagnostic: DiagnosticRevealTarget, tab?: NavTab } | undefined;
1314

1415
// webview provider
1516
context.subscriptions.push(
@@ -18,15 +19,16 @@ export function registerWebview(context: vscode.ExtensionContext) {
1819
);
1920
// show view command
2021
context.subscriptions.push(
21-
vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget) => {
22+
// shows the diagnostic in the Verification tab, or a state error in the State Machine tab when tab is 'fsm'
23+
vscode.commands.registerCommand("liquidjava.showView", async (diagnostic?: DiagnosticRevealTarget, tab?: NavTab) => {
2224
const isVisible = extension.webview?.isVisible();
2325
await vscode.commands.executeCommand("liquidJavaView.focus");
2426
if (!diagnostic) return;
2527

2628
if (isVisible) {
27-
extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic });
29+
extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic, tab });
2830
} else {
29-
pendingDiagnosticReveal = diagnostic;
31+
pendingDiagnosticReveal = { diagnostic, tab };
3032
}
3133
})
3234
);
@@ -40,7 +42,7 @@ export function registerWebview(context: vscode.ExtensionContext) {
4042
if (extension.stateMachine !== undefined) extension.webview?.sendMessage({ type: "fsm", sm: extension.stateMachine });
4143
if (extension.status) extension.webview?.sendMessage({ type: "status", status: extension.status });
4244
if (pendingDiagnosticReveal) {
43-
extension.webview?.sendMessage({ type: "revealDiagnostic", diagnostic: pendingDiagnosticReveal });
45+
extension.webview?.sendMessage({ type: "revealDiagnostic", ...pendingDiagnosticReveal });
4446
pendingDiagnosticReveal = undefined;
4547
}
4648
}
Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
import * as assert from 'node:assert/strict';
2+
import * as path from 'node:path';
3+
import * as vscode from 'vscode';
4+
import type { LJDiagnostic, StateRefinementError } from '../types/diagnostics';
5+
import type { LJStateMachine } from '../types/fsm';
6+
import type { LiquidJavaTestApi, WebviewMessage } from '../types/test-api';
7+
8+
suite('Bundled LiquidJava state machine errors', () => {
9+
test('sends the webview state errors with their machine and shows them on it from the editor', async () => {
10+
const installed = vscode.extensions.getExtension<LiquidJavaTestApi>('AlcidesFonseca.liquid-java');
11+
assert.ok(installed);
12+
const api = await installed.activate();
13+
await api.ready;
14+
15+
const workspace = vscode.workspace.workspaceFolders?.[0];
16+
assert.ok(workspace);
17+
const refinementsUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/TreeNodeRefinements.java');
18+
const callerUri = vscode.Uri.joinPath(workspace.uri, 'src/main/java/FailingTreeNodeState.java');
19+
const sameFile = (file: string, uri: vscode.Uri) => vscode.Uri.file(path.resolve(file)).fsPath === uri.fsPath;
20+
const isStateError = (diagnostic: LJDiagnostic): diagnostic is StateRefinementError =>
21+
diagnostic.type === 'state-refinement-error' && sameFile(diagnostic.file, callerUri);
22+
const subscriptions: vscode.Disposable[] = [];
23+
const nextWebviewMessage = <T>(description: string, matches: (event: WebviewMessage) => T | undefined) =>
24+
new Promise<T>((resolve, reject) => {
25+
const timeout = setTimeout(() => reject(new Error(`Timed out waiting for ${description}`)), 90_000);
26+
const done = (callback: () => void) => {
27+
clearTimeout(timeout);
28+
subscription.dispose();
29+
failure.dispose();
30+
callback();
31+
};
32+
const subscription = api.onWebviewMessage(event => {
33+
const value = matches(event);
34+
if (value !== undefined) done(() => resolve(value));
35+
});
36+
const failure = api.onFailure(() =>
37+
done(() => reject(new Error(`LiquidJava verifier crashed while waiting for ${description}`))));
38+
subscriptions.push(subscription, failure, { dispose: () => clearTimeout(timeout) });
39+
});
40+
41+
try {
42+
// hide the view first so showing it always loads a fresh webview
43+
await vscode.commands.executeCommand('workbench.action.closeSidebar');
44+
const ready = nextWebviewMessage('the webview to be ready', event =>
45+
event.direction === 'fromWebview' && event.message.type === 'ready' ? true : undefined);
46+
await vscode.commands.executeCommand('liquidjava.showView');
47+
await ready;
48+
49+
const machine = nextWebviewMessage('the refinements file state machine', event =>
50+
event.direction === 'toWebview' && event.message.type === 'fsm' && event.message.sm
51+
? event.message.sm as LJStateMachine : undefined);
52+
const stateError = nextWebviewMessage('the state error diagnostics', event =>
53+
event.direction === 'toWebview' && event.message.type === 'diagnostics'
54+
? (event.message.diagnostics as LJDiagnostic[]).find(isStateError) : undefined);
55+
const document = await vscode.workspace.openTextDocument(refinementsUri);
56+
await vscode.window.showTextDocument(document);
57+
await vscode.commands.executeCommand('liquidjava.verify');
58+
59+
const [sm, error] = await Promise.all([machine, stateError]);
60+
assert.equal(sm.className, 'javax.swing.tree.DefaultMutableTreeNode');
61+
assert.ok(error.stateMachine, 'the state error must carry its state machine');
62+
assert.equal(error.stateMachine.className, sm.className, 'errors are matched to the machine by class');
63+
assert.ok(error.stateMachine.errorContext, 'the state error must carry its error context');
64+
assert.ok(error.position && sameFile(error.position.file ?? error.file, callerUri));
65+
assert.ok(error.declarationPosition?.file && sameFile(error.declarationPosition.file, refinementsUri));
66+
67+
// the editor offers to show the state error on its state machine
68+
await vscode.window.showTextDocument(await vscode.workspace.openTextDocument(callerUri));
69+
const codeLenses = await vscode.commands.executeCommand<vscode.CodeLens[]>('vscode.executeCodeLensProvider', callerUri);
70+
const stateMachineLens = codeLenses.find(codeLens => codeLens.command?.title === 'Show in state machine');
71+
assert.ok(stateMachineLens?.command, 'state errors must have a CodeLens to show them on the state machine');
72+
assert.equal(stateMachineLens.command.command, 'liquidjava.showView');
73+
const [target, tab] = stateMachineLens.command.arguments ?? [];
74+
assert.equal(tab, 'fsm');
75+
assert.deepEqual(target.position, error.position);
76+
77+
const reveal = nextWebviewMessage('the state error to be shown on the state machine', event =>
78+
event.direction === 'toWebview' && event.message.type === 'revealDiagnostic' ? event.message : undefined);
79+
await vscode.commands.executeCommand(stateMachineLens.command.command, ...stateMachineLens.command.arguments!);
80+
const message = await reveal;
81+
assert.equal(message.tab, 'fsm');
82+
assert.deepEqual((message.diagnostic as { position: unknown }).position, error.position);
83+
} finally {
84+
subscriptions.forEach(subscription => subscription.dispose());
85+
await vscode.commands.executeCommand('workbench.action.closeAllEditors');
86+
}
87+
});
88+
});

0 commit comments

Comments
 (0)