GeezerVison

… line (#189)

Closes #187

## What changes
The Verification panel's **Expected** box and every **Found** line:
- **One line per top-level conjunct**, with `&&` at the end of each line
except the last. An `&&` inside parentheses or a string literal stays on
its line. Nothing is split when a weaker operator (`||`, `-->`, `?:`)
sits outside the parentheses, so a line never looks like a conjunct of
the whole expression.
- **A conditional outside parentheses** shows its condition on one line
and each branch on an indented line of its own (`? …`, `: …`). This is
what makes A1_09 fit.
- **Wrapped lines have a hanging indent**, so you can see where each
line starts.
- **No breaks inside names.** The VC cells used `overflow-wrap:
anywhere`, which gave `failures.siz|e()`, `compressionN|otExplicit` and
`display(host|) ==`. They now use `break-word`, so a line breaks at a
space and splits a name only when the name alone is wider than the line.
- **Narrow panel (webview at most 420 px wide).** Each binder (`∀host`)
goes above its predicate, so the predicate gets the whole width. The
card and the Found box get less horizontal padding, and the Found lines
get line-height 1.4 instead of 1.6.

This is display only. The text of every expression is the same as
before, only laid out on more lines. The hover and the CLI do not
change.

## Acceptance check: the six study tasks at the study width
Headless VS Code at 1600×900, Dark Modern, default side bar (300 px; the
error card is about 240 px). Verifier 0.0.37, the released one, which is
what this branch builds with. Each image shows main on the left and this
PR on the right. The webview is 794 px tall. "Found ends at" is the
bottom of the Found box, in webview px.

| Task | Found ends at (main → PR) |
|---|---|
| A2_10 | 503 → 453 |
| A1_38 | 575 → 544 |
| A1_01 | 562 → 521 |
| A2_04 | 413 → 414 |
| A1_56 | 498 → 473 |
| A1_09 | **996 → 740**: on main it ran below the fold |

Expected and Found are fully visible in all six, with no name broken.

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

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

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

## Verifier version
None needed. This works with 0.0.37 and with main.

## Overlap with open PRs
- **#185 (Found as facts)** may conflict. It splits each Found node into
conjunct lines in `vc-changes.ts` (`formatImplicationLines`, with its
own `splitConjuncts`), and this PR changes `renderVCLine` in the same
file.
- The two are compatible: this PR's split keeps a trailing `&&`, so a
line #185 has already split is left as it is.
- Whichever lands second should keep one `splitConjuncts`. This PR's
copy is in `highlighting.ts` and follows the same rules.
- #185's binder-hiding on continuation lines works with the stacked
binder layout.
- **#186 (Context tab)**: no overlap. This PR does not touch the Context
tab or `sections.ts`.

## Not changed
- The Locations links (file names such as
`E_OSS_A1_01_SlideRecode|r.java`) still break anywhere. They are in a
`<pre>` with `break-word`, and the names are wider than the card. This
was outside the issue.
- Top-level `||` (A1_01's Expected) is not split into lines. The issue
asks for conjuncts.

## Checks
`npm run test:unit` (127 passed; 3 new tests, each fails on main), `npm
run test:typecheck`, `npm run lint`, server `mvn -B test` (39 passed,
unchanged).

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

---------

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]>

…name (#193)

Closes #192

**Stacked on #191** (base `feat/181-declaration-notes`): it renders
#191's declared-here gloss, and it needs the same 0.0.38 bump. Retarget
this PR to `main` before #191 is merged with `--delete-branch`.

## What changes
**Server**
- `LJDiagnosticDTO` now sends two more fields for every diagnostic:
  - `messageNotes`, from `getMessageNotes()`;
- `references`, from `getReferences()`, as `SourceReferenceDTO(message,
text, start, position)`. The position counts lines and columns from 0,
like the other DTO positions.
- Both come from the verifier's generic `LJDiagnostic` API. New notes
and references therefore show up with no extension change.

**Panel (Verification tab)**
- The **message notes**, e.g. `Origin: line 134, …`, are shown under
Found and the Counterexample. Before this PR the panel did not show
notes at all.
- Every message line goes through one renderer,
`webview/message-text.ts`: the header message, notes, hints and the
declared-here gloss.
- **Code** the verifier marks with backticks is shown in the editor
font, without the backticks, with VS Code's inline-code colours
(`textPreformat`).
- Spans are parsed as the verifier's `Code.render` parses them: the same
run-of-backticks pattern, and one space of padding stripped.
- **Each reference** (`line 134`, `ArrayListRefinements.java:162`) is a
link that opens that file at that line. It is placed at the reference's
`start`; the text is not searched for, as the verifier asks. It reuses
the panel's existing `location-link` handler.
- **Hints** are now in the UI font, so their code stands out. Before,
the whole hint was monospace.
- **Header message:** it is now escaped. Before, it was put into the
HTML unescaped.

**Hover and Problems:** unchanged by this PR. See the two options below.

## Verifier version
Needs a release (0.0.38 or later) containing
**liquid-java/liquidjava#528, #530 and #533**, on top of #517 and #525
(both on main).
- `getReferences()`, `SourceReference` and the backticks come from #533.
- The Origin notes come from #528/#530.

I tested against #533's head (`1e94930`), installed as 0.0.38 into an
isolated Maven repository. Like #191, CI's server build fails until
0.0.38 is on Maven Central.

## Panel at the study width: before (#191) → after (this PR)
Both use verifier #533, with Hints open. The notes are new, the code is
set apart, and `line 134` is a link.

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

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

| A1_01 | A1_09 (hints) |
|---|---|
| <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01.png"
width="420"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_09.png"
width="420"> |

**Clicking `line 134`** in A1_38 opens line 134, `new
BufferedInputStream(stream)`:

<img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-link.png"
width="860">

Panel text of the notes (verifier #533):
```
A1_38  Origin: line 134, new BufferedInputStream(stream) makes markState(buffered) == unmarked
A1_01  Origin: line 130, writer.getDefaultWriteParam() returns compression(wParam) == compressionNotExplicit
A2_04  Origin: line 94, timeout is a parameter of checkCimReachable(String, int) with no refinement
A2_10  Origin: ArrayListRefinements.java:162, failures.size() guarantees only failures.size() >= 0
A1_56  Origin: line 69, frame.getUndoManager() says nothing about redoState(undoManager)
```
A1_09 has no Origin note.

## Hover: the two options
VS Code shows a diagnostic's message as plain text. So the diagnostic
hover and the Problems view keep the backticks.

- **A, plain text (#190):** the diagnostic message is the headline, then
the notes, then the counterexample, all plain with backticks, as rustc
writes them. One text, the same as the CLI with colour off, in the hover
and in Problems.
- **B, markdown provider (prototype on branch
`proto/192-markdown-hover`, not in this PR):**
  - The diagnostic message stays the headline only, as on main.
- The extension's `HoverProvider` adds a markdown block with the notes
and the counterexample: code spans, and `line 134` as a link.
- VS Code draws it under the problem part, so nothing is shown twice.
That holds only as long as #190's notes are not also in the diagnostic
message.

| | A: plain (#190 + #533) | B: markdown provider |
|---|---|---|
| A1_38 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-hover-a.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_38-hover-b.png"
width="430"> |
| A2_04 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_04-hover-a.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_04-hover-b.png"
width="430"> |
| A2_10 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_10-hover-a.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A2_10-hover-b.png"
width="430"> |
| A1_01 | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01-hover-a.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/193/A1_01-hover-b.png"
width="430"> |

**Recommendation: A for the study.**
- **Same text everywhere.** The hover is the one surface the baseline
shares, and the joint review's decision 5 says compared elements must be
in the hover/CLI text. A gives one string: hover = Problems = CLI with
colour off.
- **B splits the message.** It shows the message in two hover parts with
two styles: the headline plain with backticks, the notes styled. The
Problems view also loses the notes.
- **B reads better on its own:** the code is set apart, and the cause is
one click away. It is a good candidate after the study. Moving to it
means taking the notes back out of #190's diagnostic message, so the two
must not both be merged.

## Overlap with open PRs
- **#191:** the base of this PR.
- **#186** may conflict in `sections.ts`: both change the imports at the
top.
- **#189** may conflict in `errors.ts` (imports, and next to the
Expected lines) and in `styles.ts` (separate rules, so unlikely).
- **#185:** probably no textual conflict. It edits `LJErrorDTO` and the
error types in `types/diagnostics.ts`; this PR edits `LJDiagnosticDTO`
and `BaseDiagnostic`.
- **#190:** no conflict in files. It is option A of the hover (above).

## Checks
`npm run test:unit` (126 passed; the new panel test fails on the base),
`npm run test:typecheck`, `npm run lint`, server `mvn -B test` (40
passed, against #533 as 0.0.38; the new converter test fails on the
base).

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

---------

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

Closes #183. Closes #176.

## What changes

The **Found** box of the Verification tab gets plain step headers and,
when the verifier could not prove Expected, a Summary step. Every step
the verifier sends stays reachable with the arrows, as the PM decided:
"Let's show it all, we will work on those identifiers after."

- **The chain stays, one conjunct per line, from #189.** The `∀x` column
(each binder still links to its source line) and the `→` arrows are
kept, as the PM asked. The line layout comes from main's #189
(`getExpressionLines`): one top-level conjunct per line, and a
conditional's branches on indented lines. This PR does not split
anything itself.
- **"Could not prove it" says so, one step ahead.** When the verifier's
message ends with *expected … but could not prove it* (A1_56, A2_04),
Found opens on a *Summary* step that reads *Nothing is known here that
could prove Expected.* This is the wording of the verifier's Unknown
category. The `←` arrow goes back to the newest step, e.g. `∀undoManager
undoManager == #getUndoManager_result`, also when there was only one
step.
- **Every step is shown.** Found shows every step of the verifier's
derivation, oldest (*Original*) to newest, plus the Summary when there
is one. Older steps whose facts use generated names (`#if_condition`,
`#switch_selector`, `extended#1`) are shown too, as are runs of the same
pass, one step per pass.
- **Step header (#176, per the PM's decision there).** The header shows
*Original*, *Simplified*, or the name of a display step such as
*Relevant to Expected*. An (i) icon after it gives a plain-language
tooltip of what that step changed, e.g. "Replaced variables with the
values they are equal to." Raw pass names (`Binder`, `Substitution`) are
no longer shown. The tooltips cover every pass verifier 0.0.38 names:
Substitution, Function Substitution, Binder, **Known Enum Values**,
Folding, Arithmetic, Logical, Constraint, and the display step Relevant
to Expected.

Steps on the six study exercises (main → this PR). Each count is the
verifier's own step count, plus one for the Summary:

| Exercise | main | this PR |
|---|---|---|
| A1_56 (could not prove it) | 19 | 20 (Summary + 19) |
| A2_04 (could not prove it) | 6 | 7 (Summary + 6) |
| A1_09 | 10 | 10 |
| A1_01 | 7 | 7 |
| A1_38 | 4 | 4 |
| A2_10 | 3 | 3 |

**No step repeats the one before it.** The verifier records a step only
when a pass changes the chain (`VCSimplification.simplifyOnce` returns
the same result when the chain is equal). So the client needs no check
for identical steps. A step can still look the same as the one before
when the pass only changed a row Found does not draw, such as
`∀#if_condition true →`. Such a step is shown anyway.

## Changes in this rework

- **Every step is shown (PM's decision).** The filter that hid older
steps with generated names is removed. So are the merging of runs of the
same pass into one step and the de-duplication of steps that looked like
the step before. Its code (`getVCSteps`, `sameLines`, `GENERATED_NAME`)
and its test are gone, and `vc-changes.ts` is back to main. Before this
rework, A1_56 showed the Summary and 1 step, A1_09 1 step, A1_01 2 and
A1_38 1.
- **Generated names are left for later.** `#if_condition`,
`#switch_selector` and instance tags like `extended#1` now show in the
older steps. #175 (line tags) and #195 (hover explanations) will handle
them.
- Earlier in this rework: rebased on main (verifier 0.0.38, #189, #190,
#191, #186). The Summary is keyed on the message, not on `errorCategory`
(see below), so **this PR is client-only**.

## Why the client, not the verifier

The verifier's messages already leave generated names out: the hover of
all six study exercises reads fine. The header and Summary only change
how the view presents the steps the verifier sends.

## Screenshots (headless VS Code, light theme, verifier 0.0.38)

Before: main (e333873). After: this branch (af43c9c).

**A1_56** (could not prove it)

| Before (19 steps) | Before, oldest step | After: opens on the Summary
(20/20) | After, one step back (19/20) | After, oldest step (Original,
1/20) |
|---|---|---|---|---|
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-before-oldest-step.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after-back.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_56-after-oldest-step.png)
|

**A1_09** (path condition and state)

| Before (10 steps) | After: Relevant to Expected (10/10) | After, one
step back (9/10) | After, oldest step (1/10) |
|---|---|---|---|
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after-back.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_09-after-oldest-step.png)
|

**A2_10** (refinement error, three steps on both)

| Before | After, Simplified 3/3 | After, Original 1/3 |
|---|---|---|
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_10-after-original.png)
|

<details><summary>A1_01, A1_38, A2_04</summary>

| | Before | After | After, one step back | After, oldest step |
|---|---|---|---|---|
| A1_01 (7 steps) |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after-back.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_01-after-oldest-step.png)
|
| A1_38 (4 steps) |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after-back.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A1_38-after-oldest-step.png)
|
| A2_04 (Summary + 6) |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after-back.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/185/A2_04-after-oldest-step.png)
|

</details>

## For the PM

- **When should the Summary show?** It is keyed on the message ending in
*but could not prove it*, not on `errorCategory`. In 0.0.38 the two
differ for some state errors. For example, if Found states only a
non-state ghost of the receiver (`size(b) > 0`), the category is
`unknown` but the message reads *found `size(b) > 0` but expected
`open(b)`*. The message is what the hover shows, so it decides here. For
refinement errors they agree, as they do on all six study exercises. Is
keying on the message right?

## Tests

`vc-implications.spec.ts` has two tests, each failing on main:
- every step of the verifier is shown, including an original chain with
`#if_condition` and two Binder steps in a row, each under *Original*,
*Simplified* or *Relevant to Expected* with its tooltip (it also fails
on the previous head, 55510f8, which hid these steps);
- the Summary when the message says *could not prove it*, with the chain
one step back.

The test for skipping steps with generated names and merging pass runs
is removed with that code.

Local results on af43c9c: `npm run test:unit` (134 passed),
`test:typecheck`, `lint`, server `mvn -B package` (42 tests),
integration `xvfb-run -a npm test` on VS Code 1.82.0 (minimum; 9 + 1
passing). Codex review of this rework: one round, whose only finding
(the Summary keyed on the message) was declined as in rounds 1 and 2.

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

---------

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

…an error alike (#196)

Closes #175

Verifier 0.0.38 (liquid-java/liquidjava#493, already the dependency on
main) names variables as in code and, only when an error has several
values of one name, tags the others with the line their value comes
from: `preview@51`. The message and the Context tab already used those
names. The rest of the panel did not: the server formatted the Expected,
the Found steps, the counterexample and the translation table with the
verifier's default formatter. That formatter numbers clashes within each
expression, so the Found of A3_07 showed three different values of
`preview` all as `∀preview`, and `preview#1` meant a different value on
each line.

## What 0.0.38 sends
- **Tag format:** `x@51`. When tagged values share a line, `x@25#1`,
`x@25#2`; with no line, `x#2`. A call argument can carry one too:
`failures.size()@84`. No Unicode superscripts any more.
- **Where:** the message, the counterexample in the message, the message
notes and hints, and the Context tab (`ContextDisplay`, merged in #186)
already use the names. `LJError.getDisplayNames()` gives the error's
names for refinement and state refinement errors; nothing else is
pre-formatted for the IDE.

## What changes
**Server** (`server/src/main/java/dtos`)
- `RefinementErrorDTO` and `StateRefinementErrorDTO` format the
expected, each step's binder and predicate (`VCImplicationDTO`), and the
counterexample with `error.getDisplayNames()`.
- `TranslationTableDTO` keys each entry by the error's name for it
(`preview@51`), so a tagged binder still opens its source. Errors
without names keep the plain key.

**Webview**
- A tag is drawn as a subscript: `preview` with a small `l51` below,
titled "value of preview at line 51" (`x@25#2` → `l25#2`, "value 2 of x
at line 25"). This applies in every highlighted expression (Expected,
Found, steps, counterexample, Context), in the binders, and in the code
of messages, notes and hints. Copy, the hover and the Problems panel
keep the ASCII `preview@51`.
- The step diff keeps `preview@51` as one token, so a changed tag
highlights its whole variable.
- String and character literals are kept whole when highlighting and
diffing, so `"a@1"` is not read as a tag.
- The regexes no longer match `⁰-⁹`.
- The Context tab's Name column renders a variable without a source
position the same way as one with a position (before, it was raw text).
- Rows the error mentions are still marked in the Context tab: the
translation-table keys are compared without their tag, as before.

## Against the issue's to-do
- Render the tag: done (subscript + tooltip). **Click-to-source:** works
on binders (`∀preview@51`) through the re-keyed translation table. A tag
inside a predicate shows only the tooltip, because the highlighter has
no translation table. The line number is in the tag itself.
- Tokenize as one identifier: done (step diff and highlighter). The
Unicode superscript handling is gone.
- **Context view: already done** by #186 (`ContextDisplay` with
`DisplayNames` and `ContextHistory.lineOf`). This PR only renders its
tags the same way.
- Translation table keyed by display name: done.
- **Bump the verifier: already done**, main depends on 0.0.38.

## Screenshots (headless VS Code, light theme, verifier 0.0.38)
**A3_07 ScannerOutputStage**, the study exercise with several values of
`preview`.

| | before (main) | after |
|---|---|---|
| Found, a step back (9/10) |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-step.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-step.png)
|
| Found, original (1/10) |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-original.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-original.png)
|
| Context tab |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-before-context.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A3_07-after-context.png)
|

**A2_08 LogWindow**, plain names (no change, as for every other study
exercise):

| before (main) | after |
|---|---|
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A2_08-before.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/175/A2_08-after.png)
|

## Not in this PR
- Explaining generated names such as `#if_condition` (#195).
- **Different scopes.** The Context tab names variables per context
(declared variable plain) and the error per error (latest shown value
plain). The same value can be `preview@54` in the Context tab and
`preview` in the error, as in the A3_07 screenshots. Making them agree
would mean a verifier change.

## Expected conflicts
- #185 (`study-found-box`): merges cleanly with its current head. It
changes `vc-implications.ts` and `styles.ts`; this PR adds one rule to
`styles.ts` and changes `TOKEN_PATTERN` and `renderBinder` in
`vc-changes.ts`. Any conflict would be in `styles.ts` (adjacent rules).
- #193 is merged; this PR changes one line of `message-text.ts`.

## Tests
- Server `DiagnosticConverterTest`: verifies a `b = -b` fixture and
checks that the message, every Found step (`∀b@6 b@6 == 8`, `∀b@7 b@7 ==
b@6 && b@7 > 0`, `∀b b == -b@7`), the expected, the counterexample and
the translation-table keys use the same names. On main the steps read
`∀b b == b#1 && b > 0`.
- Client `vc-changes.spec`: tags render as subscripts with their tooltip
(also after a call and with a number). A changed tag is diffed with its
variable. A literal is left alone. `diagnostics.spec`: a tag in a
message's code, next to a literal. `context.spec` was updated to the
rendered tag.
- Local: `npm run test:unit` (134), `test:typecheck`, `lint`, `mvn -B
package` (44), `VSCODE_TEST_VERSION=minimum xvfb-run -a npm test` (9 + 1
passing).

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

---------

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