GeezerVison

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