Put the State Machine tab 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');

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