[CatarinaGamboa]

Description

Closes #117.

When the State Machine view is opened from a state refinement error, it now starts focused on the error.

• Focused view. It shows the found state, the required states, and the states on the shortest path between them. Initial arrows, unrelated states and unrelated self-loops are left out. A self-loop is kept when it starts on a required state and is labelled with the called method.
• Marks. Each mark has an icon and text, so it reads without colour.
  • The found state is red: "◉ Found for this receiver at the call".
  • Required states are green: "✓ Required for this call".
  • The rejected call ("⊘ root.getFirstChild()" / "Call rejected from this state") is a dashed red note joined to the found state by a dashed line with no arrow. It is never drawn as a transition, and it appears even when the method has no transition or shares a merged label.
• Uncertain Found. When Found does not establish one state, a dashed box shows the Found condition. Candidate states are marked "? Possible", and no single state is red. A state that is both possible and required gets one combined label.
• Summary and toggle. A text summary above the diagram lists the call, Found and Required. "Show full diagram" and "Focus on error" switch views, and pan and zoom are unchanged. The full view keeps the same marks and still highlights where the called method is allowed.
• Identifying the call. The call is identified from the verifier's error context (liquidjava-fsm 0.1.4: receiver, expectedStates, expectedCondition, foundCondition, definiteFoundState), not from transition label text. With an older context the view behaves as before.
• Code. The focus logic is in client/src/webview/diagram-focus.ts. It works on one machine at a time, so multiple @StateSet support can reuse it.
• Dependency. Bumps liquidjava-fsm to 0.1.4.

Tests

Run against liquidjava-fsm 0.1.4 and verifier 0.0.35 from Maven Central:

• npm run lint and npm run test:typecheck: clean.
• npm run test:unit: 61 passed in 7 files. The 25 new tests are in diagram-focus.spec.ts, styles.spec.ts, fsm.spec.ts and script.spec.ts.
• npm test (VS Code): 8 + 1 passing.
• Server mvn test: 24 passing.
• Local smoke test: passed.

The new tests cover:

• the issue's DefaultMutableTreeNode example;
• a 7-state Socket-like machine whose focus leaves out unrelated states;
• a Found that does not establish one state;
• a state that is both possible and required;
• a method missing from the general diagram, and a merged label;
• the allowed self-loop;
• the computed red/green outlines;
• switching between full and focus views, and opening a second error after switching;
• an older error context without the new fields.

Also checked in headless VS Code on the DefaultMutableTreeNode example from the issue, using the real verifier output. The view opens on childrenAllowed(root), the rejected getFirstChild() and maybeHasChildren.

Independently reviewed; all five findings were fixed with regression tests.

Known limits

• In the default narrow sidebar, the focused diagram is scaled down and stays legible.
• Clicking a diagram button while Mermaid is still rendering can rarely log a render error. This already happens on main with the orientation and conditions buttons.
• Show state machine errors in the State Machine view #155 touches the same webview files; whichever PR merges second will be rebased.

🤖 Generated with Claude Code