GeezerVison

… a call sequence works (#524)

Closes #518
Closes #519

## What and why
Changes to the state hints in `StateHints` (display and choice of hints
only; the VC, verdict and category are unchanged):

1. **Call sequences name only the state they lead to** (#519): `Call S
before this call; afterwards <state>`. The "from" part is gone, since
the Found already shows it. In A1_09 it listed every state of the set
(`from display(host) == notDisplayable or display(host) ==
displayable`). "Afterwards" is the machine's `after` state for the
changed sets, so the hint only states what the machine computes after
the calls, and no `!=` is turned into `==`. The value form from #517
stays (`markState(buffered) == marked`). Classes with no named set read
`afterwards f is open`.
2. **A deciding argument is written as the call** (#519): when a step's
condition is `param == c` for the method's only parameter, and `c` names
no variable, the step is written
`wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)`. Any other
condition keeps `r.set(int lo, int hi) with lo < hi`.
3. **No GUARD hint when a CALL_SEQUENCE hint exists** (#518). Wrapping
the call in the check skips it in exactly the failing case. In A1_09 the
verifier accepts that fix and the study grader marks it INCORRECT.
Before, the guard was dropped only for a single known state. The
unknown-state hints (A1_56) do not change: its guard stays, since it has
no call sequence and the guard is the reference fix.
4. **Guard wording** (#518): `Guard this call with if (<check>); inside
it, <state>`. This replaces "when it returns false", which was ambiguous
next to `!host.isDisplayable()`.
5. **AVAILABLE_CALLS ("can call") is dropped when any other hint is
given** (#519). FINAL_STATE is unchanged.

## Study tasks (CLI, before = main, after = this branch)
Each task still gives exactly one error, on its `reportedLine`. A2_10,
A2_04, practice and practice2 are unchanged.

**A1_38**
```
before:
  - Call buffered.mark(int) before this call to move buffered from markState(buffered) == unmarked to markState(buffered) == marked
  - When stream(buffered) == open and markState(buffered) == unmarked, buffered can call: read(), read(byte[], int, int), skip(long), available(), mark(int), ...
after:
  - Call buffered.mark(int) before this call; afterwards markState(buffered) == marked
```
**A1_01**
```
before:
  - Call wParam.setCompressionMode(int mode) with mode == ImageWriteParam.MODE_EXPLICIT before this call to move wParam from compression(wParam) == compressionNotExplicit to compression(wParam) == compressionExplicit
  - When tiling(wParam) == tilingNotExplicit and compression(wParam) == compressionNotExplicit, wParam can call: setTilingMode(int), setCompressionMode(int) (and possibly others)
after:
  - Call wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT) before this call; afterwards compression(wParam) == compressionExplicit
```
**A1_09**
```
before:
  - Call host.dispose() before this call to move host from display(host) == notDisplayable or display(host) == displayable to display(host) == notDisplayable
  - Call host.removeNotify() before this call to move host from display(host) == notDisplayable or display(host) == displayable to display(host) == notDisplayable
  - Guard this call with if (!host.isDisplayable()): when it returns false, display(host) == notDisplayable
  - When display(host) == notDisplayable or display(host) == displayable, host can call: pack(), dispose(), addNotify(), removeNotify() (and possibly others)
after:
  - Call host.dispose() before this call; afterwards display(host) == notDisplayable
  - Call host.removeNotify() before this call; afterwards display(host) == notDisplayable
```
`host.dispose()` is still the first hint. `analysis/check-fixes.py
--selftest --task A1_09` passes 8/8 and grades the plain `dispose()` fix
(P01) CORRECT.

**A1_56** (the guard stays)
```
before:
  - The state of undoManager is unknown here, and this call needs redoState(undoManager) == redoable
  - Guard this call with if (undoManager.canRedo()): when it returns true, redoState(undoManager) == redoable
after:
  - The state of undoManager is unknown here, and this call needs redoState(undoManager) == redoable
  - Guard this call with if (undoManager.canRedo()); inside it, redoState(undoManager) == redoable
```

## IDE
Hints reach vscode-liquidjava as plain message text, so they show there
with no extension change. There are no screenshots, because nothing in
the extension's layout changes.

## Tests
The exact-message expectations in `TestStateHints` are updated. Each of
these fails on main: the new wording, no "can call" next to another
hint, and `setCompressionMode(2)` / `chain.pick(1)` for the argument
form. One case is added to the existing `ErrorStateHintGuards` fixture:
`reachableOnEveryPath`, the A1_09 shape (path-dependent state, a call
that reaches the needed state, a query). On main it gives a sequence, a
guard and "can call"; now it gives only the sequence. The full suite
passes locally (728 tests).

## Open for the PM
- The unknown-state hints (`anyState`, used by A1_56) can also list a
call sequence after the guard. #518 scopes the rule to `forCall`, so the
guard is kept there. None of the study tasks has both.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

The server sends the verifier's declaration positions and declaration notes
(the "where ... means ..." lines) of refinement and state errors, and the
Locations section shows a link to every position, with the notes under them.

Needs liquidjava-verifier 0.0.38: getDeclarationNotes() comes from
liquid-java/liquidjava#517 and getDeclarationPositions() from
liquid-java/liquidjava#525.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

Closes #188

## What changes
The editor diagnostic that `LJDiagnosticsHandler` publishes now carries:
1. the headline (`<title>: <message>`), as before;
2. then each of the verifier's **message notes**,
`LJDiagnostic.getMessageNotes()`, one per line;
3. then the verifier's **counterexample**, `getCounterexampleStr()`,
when it has one.

That text is what the hover and the Problems view show. **Hints are left
out**, since they stay collapsed in the panel by design.

The server reads the verifier's generic `LJDiagnostic` API, not a
per-error list. So any note the verifier adds later appears in the hover
with no extension change. That includes the planned From note
(liquid-java/liquidjava#522), and a counterexample for state errors once
the verifier gives one.

## Before → after (hover text, verifier 0.0.37)
**A2_04**
```diff
  Refinement Error: expected timeout >= 0 but could not prove it
+ Counterexample: timeout == -1
```
**A2_10**
```diff
  Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0
+ Counterexample: failures.size() == 0
```
A1_38, A1_01, A1_56 and A1_09 are unchanged. Their errors have no
message notes and no counterexample in 0.0.37 or main.

| | Before | After |
|---|---|---|
| A2_04 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_04-before.png"
width="440"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_04-after.png"
width="440"> |
| A2_10 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_10-before.png"
width="440"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/190/A2_10-after.png"
width="440"> |

(Headless VS Code, 1600×900, Dark Modern.)

## Verifier version
**0.0.37**, already released. `getMessageNotes()` and
`getCounterexampleStr()` are both in it, and the branch builds with the
current pom. Today the only message notes are the `where <alias> means
…` lines of refinement errors that use aliases, and no study task has
one. The From note will come with a later verifier release.

## Open question for the PM
The issue lists the `where … means …` gloss among the notes. In the
verifier, the gloss is a **declaration note** (`getDeclarationNotes()`,
liquid-java/liquidjava#517, needs 0.0.38). It explains the "declared
here" excerpt, which the hover does not show. So this PR shows only the
message notes, as specified. If the hover should also show the gloss,
that is one more `lines.addAll(diagnostic.getDeclarationNotes())`, but
it needs the 0.0.38 bump that #191 makes.

## Overlap with open PRs
Server only, in `LJDiagnosticsHandler`. No conflict with #185, #186,
#189 or #191.

## Checks
Server `mvn -B test` (40 passed; new `LJDiagnosticsHandlerTest`, which
fails on main), `npm run test:unit` (124 passed), `npm run
test:typecheck`, `npm run lint`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

Closes #181

## What changes
- **Server.** `RefinementErrorDTO` and `StateRefinementErrorDTO` now
send:
- `declarationPositions`, from `LJDiagnostic.getDeclarationPositions()`;
- `declarationNotes`, the `where … means …` lines, from
`getDeclarationNotes()`.

Both are read through the verifier's generic `LJDiagnostic` API. So when
the verifier adds notes or positions, they appear with no extension
change. `declarationPosition`, the first position, stays as it is for
the State Machine view.
- **Client.** The Locations section links to **every** declaration
position, then shows the notes under the links, muted and with a hanging
indent. A declaration in value form (`doorState(this) == closed`), or
one with unnamed sets, has no notes, so nothing changes for it.
- **Fallback to one position.** The verifier's default
`getDeclarationPositions()` returns the single
`getDeclarationPosition()`. Refinement errors and any other error with
one declaration therefore show one link, as before.

## Verifier version: needs 0.0.38 (not yet released)
| Part | Verifier change |
|---|---|
| `declarationNotes` (the gloss) | liquid-java/liquidjava#517 (merged in
main) |
| `declarationPositions` (every `from`, e.g. A1_01 lines 110 and 111) |
liquid-java/liquidjava#525 (**open**) |

The pom is bumped to `0.0.38`, so **CI's server build fails until 0.0.38
is on Maven Central**. Please merge this PR only after a verifier
release that has both #517 and #525. If #525 is not merged, drop the
`declarationPositions` lines from the two DTOs (one line each) and use
`declarationPosition` in `renderLocation` again. The gloss part only
needs #517.

I tested it locally against #525's head (`9d1bb1e`, which contains
main), installed as 0.0.38 in an isolated Maven repository.

## Before → after (Locations section, at the study width)
Before is main, with its server built on verifier main. After is this PR
on #525's head. Headless VS Code, 1600×900, Dark Modern, default side
bar.

**A1_01**: both `from`s, each with its gloss
```diff
  E_OSS_A1_01_SlideRecoder.java:136
  ImageWriteParamRefinements.java:110
+ ImageWriteParamRefinements.java:111
+ where compressionExplicit(this) means compression(this) == compressionExplicit
+ where compressionTypeSet(this) means compression(this) == compressionTypeSet
```
**A1_38**
```diff
  E_OSS_A1_38_FormatReaderManager.java:157
  BufferedInputStreamRefinements.java:81
+ where marked(this) means markState(this) == marked, open(this) means stream(this) == open
```
**A1_56**: `+ where redoable(this) means redoState(this) == redoable`
**A1_09**: `+ where notDisplayable(this) means display(this) ==
notDisplayable`
**A2_04**: unchanged. `@Refinement("_ >= 0")` has no gloss. The missing
Hint in the after shot comes from #525, not from this PR.

| A1_01 | A1_38 |
|---|---|
| <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_01.png"
width="420"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_38.png"
width="420"> |

| A1_56 | A1_09 |
|---|---|
| <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_56.png"
width="420"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A1_09.png"
width="420"> |

<details><summary>A2_04</summary>

<img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/191/A2_04.png"
width="420">
</details>

The A1_01 and A1_09 shots are scrolled to Locations. The yellow outline
is the focus left on Hints by the screenshot script.

## Overlap with open PRs
- **#186 (Context tab)** may conflict in
`client/src/webview/views/sections.ts`. It changes
`renderVariableHighlightButton` and the imports, right after
`renderLocation`, which this PR edits.
- **#185 (Found as facts)** may conflict in
`client/src/types/diagnostics.ts`. Both PRs add fields to
`RefinementError` and `StateRefinementError`, in nearby hunks. No
conflict in logic.
- **#189 (panel wrapping)**: the notes are in the Locations `<pre>`,
which keeps `break-word`, so a long `compressionExplicit(this)` can
still wrap inside the name at 240 px (see A1_01). They do not share
files apart from `styles.ts`, in separate rules.

## Checks
`npm run test:unit` (125 passed; the new test fails on main and also
checks the copied text), `npm run test:typecheck`, `npm run lint`,
server `mvn -B test` (39 passed, against #525 as 0.0.38; the converter
test now also checks the notes and the positions).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>