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..ffd4115 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'); 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 { `;