GeezerVison

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