GeezerVison

…argument it gives (#530)

Closes #522, part 3: **origin note F4**, a value returned by a call.
Design:
#522 (comment)

**Stacked on #528** (`CallResult` and the Origin rename). Retarget this
PR to `main` before #528 is merged with `--delete-branch`, or GitHub
closes it.

A refinement error whose Expected is about a **call argument that is
itself a call to a refined method** now says what that method's return
refinement guarantees. This is the UX sign-off's amendment 1 for A2_10:
instantiated as the error writes it, with the ghost-defining conjunct
dropped.

## When it is printed
For each variable of Expected that is an argument instance with no
variable of its own (shown as the call), holding the `CallResult` of a
refined method whose refinement has a source position. Locals assigned
from a call are left to #528's state notes. A refinement-error form for
them (`Origin: line 44, read() guarantees only n >= -1`) is a question
for the PM.

It is also left out when the refinement still names an argument the
verifier calls after the callee's parameter (`twice(0)` for `_ == b *
2`), which would read as that parameter.

**Text:** `Origin: <File>:<line>, <call> guarantees only <R'>`, or
`Origin: <File>:<line>, <call> guarantees nothing about <call>` when
nothing is left. This is the shape #528 gives every origin note.

**Why "only" is sound.** `R'` is the instantiated return refinement
minus each conjunct `_ == g(…)` where all hold:
- `g` is a declared ghost (`@Ghost`), and never a built-in name like
`length`, even when some class declares a ghost of that name;
- `g`, on any arguments, appears in no other conjunct and not in
Expected. Any arguments, because an alias of the receiver may constrain
the ghost under another name;
- every fact of the error's Found that applies `g` is the argument's own
equality with it;
- no alias application in the refinement, Expected or Found may hide a
use of `g`.

Then nothing constrains `g(…)` but that equality, and ∃g. (_ == g ∧
Q(_)) ≡ Q(_), since `g := _` is a witness. So `R'` is exactly what the
refinement says about the value. Nothing else is dropped. Otherwise the
equality is kept, e.g. `Origin: …, count(xs) guarantees only count(xs)
== length(xs)`.

## A2_10, before and after
```diff
 Refinement Error: found failures.size() == size(this.failures) && failures.size() >= 0 but expected failures.size() > 0
+  Origin: ArrayListRefinements.java:162, failures.size() guarantees only failures.size() >= 0
 75 |     public Failure get() {
```
This is the amended mock-up, in the Origin shape. The other notes are
unchanged from #528, and every task still gives one error on its
`reportedLine`.

Across all refinement-error fixtures, the only new notes are the two
call arguments in `classes/found_binders_error`: `items.size()` and
`count()`.

## Test

`TestOriginNotes.callArgumentIsTracedToWhatItsReturnRefinementGuaranteesAboutIt`,
on the existing `classes/found_binders_error` (the A2_10 reproducer,
line 25): `Origin: ArrayListRefinements.java:13, items.size() guarantees
only items.size() >= 0`. It fails without the change.

`mvn test`: 737 run, 0 failures.

## Conflicts
- With #520/#521 (another agent, `RefinementError` headline): none in
the files changed here.
`MethodsFunctionsChecker.createVariableRepresentingArgument` gets one
line, and `Utils` gets `isBuiltin(name)` over its existing
`DEFAULT_NAMES`.

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

---------

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

…fer to (#533)

Closes #532. **Stacked on #530** (→ #528 → `main`). Retarget it to
`main` before #530 is merged with `--delete-branch`.

Every message that shows code now marks it with backticks, inside the
message string:
- headlines (`found … but expected …`, `expected … but could not prove
it`);
- hints;
- origin notes;
- the declared-here gloss (`where … means …`);
- alias `where` lines;
- counterexamples.

## How each client sees it
- **Plain text** (`getMessage()`, `getMessageNotes()`, `Hint.message()`,
`getCounterexampleStr()`, `getDeclarationNotes()`, and so the Problems
tab and the hover): the string with backticks, as rustc writes its
messages.
- **CLI:** each span in blue (the existing `Colors.BLUE`), without
backticks. The backticks stay when colour is off: `NO_COLOR` set
(https://no-color.org) or no console (output piped or redirected). The
colour switch applies to code spans only; the CLI's other colours are
unchanged.
- **IDE:** the same backticked strings, plus
`LJDiagnostic.getReferences()`, a `List<SourceReference>` with one entry
per line reference. See below.

**Escaping:** `Code.of` fences code that holds backticks with a longer
run, and pads it with one space on each side when it holds a backtick or
starts or ends with a space: ``` `` c == '`' `` ```. `Code.render`
strips exactly that padding, so it shows any non-empty code exactly as
marked.

## Source references (for vscode-liquidjava#192)
`record SourceReference(String message, String text, int start, String
file, int line, int column)`:
- `message`: the whole message line it belongs to, exactly as
`getMessageNotes()` or `Hint.message()` gives it;
- `text`: the words of `message` that name the place, e.g. `line 134` or
`ArrayListRefinements.java:162`;
- `start`: where `text` starts in `message`, as a UTF-16 index (a
Java/JS string index), so `message.substring(start, start +
text.length())` is `text`. Use it instead of searching, because the code
of a call can hold the same words (`d.lock("line 18")` on line 18);
- `file`: the absolute path; `line`, `column`: 1-based, from Spoon.

Who carries one:
- every origin note: the call, parameter, constructor or
return-refinement declaration it names;
- the deciding-argument hint (`… on line 20 decides …`), through the new
`Hint.reference()`, which is null for other hints.

`getReferences()` returns the notes' references first, then the hints'.

## Before → after (CLI piped, so backticks shown)
```text
A1_38  State Refinement Error: found `stream(buffered) == open && markState(buffered) == unmarked` but expected `markState(buffered) == marked && stream(buffered) == open`
         Origin: line 134, `new BufferedInputStream(stream)` makes `markState(buffered) == unmarked`
         - Call `buffered.mark(int)` before this call; afterwards `markState(buffered) == marked`
         where `marked(this)` means `markState(this) == marked`, `open(this)` means `stream(this) == open`
A1_01    Origin: line 130, `writer.getDefaultWriteParam()` returns `compression(wParam) == compressionNotExplicit`
         - Call `wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT)` before this call; afterwards `compression(wParam) == compressionExplicit`
A2_04  Refinement Error: expected `timeout >= 0` but could not prove it
         Origin: line 94, `timeout` is a parameter of `checkCimReachable(String, int)` with no refinement
          --> Counterexample: `timeout == -1`
A1_56    Origin: line 69, `frame.getUndoManager()` says nothing about `redoState(undoManager)`
         - Guard this call with `if (undoManager.canRedo())`; inside it, `redoState(undoManager) == redoable`
A2_10  Refinement Error: found `failures.size() == size(this.failures) && failures.size() >= 0` but expected `failures.size() > 0`
         Origin: ArrayListRefinements.java:162, `failures.size()` guarantees only `failures.size() >= 0`
```
For all eight tasks (six study tasks and both practice tasks), the
output with backticks removed is byte-identical to #530's. Each task
still gives exactly one error, on its `reportedLine`. On a terminal the
spans are blue and the backticks are gone. With `NO_COLOR=1` the
backticks stay.

## Changes
- `Code` (`of`, `render`), `SourceReference`, and `Colors.enabled()`.
- `LJDiagnostic`:
  - `addMessageNote(SourceReference)` and `getReferences()`;
- `toString` renders the message, notes, counterexample, hints and
declaration notes.
- Marked at the leaves where messages are built:
  - `ErrorMessage` (both headline frames);
  - `RefinementError` (counterexample, alias lines);
  - `AuxStateHandler.addMeanings` (gloss);
- `StateHints`: each state name, call, receiver and constructor, with
the prose words `or`, `and`, `then`, `with` left unmarked;
  - `OriginNotes`/`StateOrigin`, whose notes are now `SourceReference`s.
- `NotFoundError` marks the missing name and the suggestion (``Alias
`Positiv` could not be found``, ``Did you mean `Positive`?``).
- Not marked: the other error kinds (state conflicts, syntax errors) and
warnings, which the issue does not list. They are a follow-up if wanted.

## Tests
- 59 existing expectations gained backticks. Each change was made by a
script that accepts a new string only if removing its backticks gives
exactly the old one.
- `TestStateHints.assertHints` compares kind and message.
- New tests, each failing without the change:
  - `CodeTest` (fence, colour on and off);
  - `TestOriginNotes.noteNamesTheLineOfTheCallForClientsToLinkTo`;
  - a reference check in the deciding-argument hint test.

`mvn test`: 740 run, 0 failures.

## Conflicts
- **#524 and #525 are merged**, and this branch sits on top of them (via
#528's rebase), so it does not conflict with them. The lines of their
code it changes are:
- `StateHints.java`, on main: the hint templates at 116–119, 131–132,
182–184, 234, 239–240, 249, 252, 258, 260, 269, 295–297, 301, 303–305,
349, and `stateName` at 387–389;
- `RefinementError.java`, on main: 71 (counterexample) and 123 (alias
`where` lines);
  - `ErrorMessage.java` 39–41 (headline);
  - `AuxStateHandler.java` 865–866 (gloss).
- With the #529 agent's work: both may touch
`VCChecker.throwStateRefinementError`. This PR changes only the notes'
parameter type there.

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

---------

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

…name

The server sends each diagnostic's message notes and the source references
of its notes and hints. The panel shows the notes under Found, and renders
every message line (headline, notes, hints, declared-here gloss) with the
code the verifier marks in backticks in the editor font and each reference,
such as `line 134`, as a link that opens that line.

Needs a liquidjava-verifier release with liquid-java/liquidjava#528, #530
and #533.

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

…name

The server sends each diagnostic's message notes and the source references
of its notes and hints. The panel shows the notes under Found, and renders
every message line (headline, notes, hints, declared-here gloss) with the
code the verifier marks in backticks in the editor font and each reference,
such as `line 134`, as a link that opens that line.

Needs a liquidjava-verifier release with liquid-java/liquidjava#528, #530
and #533.

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

…name

The server sends each diagnostic's message notes and the source references
of its notes and hints. The panel shows the notes under Found, and renders
every message line (headline, notes, hints, declared-here gloss) with the
code the verifier marks in backticks in the editor font and each reference,
such as `line 134`, as a link that opens that line.

Needs a liquidjava-verifier release with liquid-java/liquidjava#528, #530
and #533.

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