GeezerVison

… as markdown, and code in the view as in the hover (#198)

Closes #197

## What changes
The editor hover shows a LiquidJava error as one markdown card: VS
Code's own problem part holds only the **title** (it renders that
message as plain text), and the extension's markdown part under it holds
the **headline**, the **origin notes**, the **counterexample** and the
**hints**:
- **code** the verifier marks with backticks is inline code (editor
font), without the backticks;
- each **line reference** (`line 134`) is a link that opens that file at
that line, from the structured `references` (`SourceReferenceDTO`), not
a text search;
- hints get a **Hint** / **Hints** heading, as in the panel, and several
call sequences are listed under "Any one of these:";
- everything else is escaped, so `*`, `_`, `<`, `|`, `#` in expressions
stay literal.

In the **LiquidJava view**, the code in the Origin line and in the hints
gets the look of inline code in a markdown hover
(`textCodeBlock.background`, inherited colour) instead of the
preformatted-text colours, which drew grey boxes around it in light
themes.

Before this PR, the hints were not in the editor hover at all, and the
notes and counterexample were plain text with raw backticks.

**Server:** the diagnostic message is the title alone
(`LJDiagnosticsHandler.diagnosticMessage`). This is what the Problems
tab, F8 and the squiggle show; the headline, the notes and the
counterexample are in the hover's card and in the view.

**Shared parsing.** The code-span and reference parsing that #193 wrote
for the panel moves from `webview/message-text.ts` to
`utils/message-text.ts` (`splitMessageText`, no `vscode` import, so both
bundles use it). The panel renders the segments as HTML, the hover as
markdown (`utils/message-markdown.ts`, `formatDiagnosticMarkdown`). The
grouping of call sequences into options (`groupHints`) moves there too.

**Trust.** The links are `file:` URIs with an `#L<line>,<col>` fragment,
which VS Code opens without a command, so the markdown part is **not
trusted** (no `isTrusted`, no command links). The existing refinement
hover keeps its own trusted `MarkdownString`; the diagnostic card is a
separate part of the hover.

## Design choice
VS Code's diagnostic hover is always plain text, and the same string is
the Problems tab entry. Rendering the headline in markdown without
showing it twice means the diagnostic itself carries only the title, so
the **Problems tab and the problem view (F8) show the error type**, not
the headline (screenshot below). The PM chose the card over the Problems
tab text (2026-11-11); putting `Title: headline` back in the diagnostic
is a one-line change in `diagnosticMessage` if that is ever wanted.

## Screenshots
Headless VS Code (openvscode 1.109), verifier 0.0.38, study task A1_38,
cursor on the error. Before = `main` + the first version of this PR
(hints only); after = this PR.

| | Before | After |
|---|---|---|
| Hover, dark | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-before-dark.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-card-dark.png"
width="430"> |
| Hover, light | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-before-light.png"
width="430"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-hover-card-light.png"
width="430"> |
| Problems tab, dark | (headline + notes + counterexample as plain text)
| <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-problems-card-dark.png"
width="430"> |
| View, dark | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-before-dark.png"
width="300"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-after-dark.png"
width="300"> |
| View, light | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-before-light.png"
width="300"> | <img
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/197/A1_38-panel-after-light.png"
width="300"> |

The first version's screenshots (hints only, E_A3_07 with a clickable
`line 51`, A1_09 with two call sequences) are in the PR's history under
`pr-screenshots/197/*-after.png` and `*-link.png`.

## Not in this PR
- The squiggle's range ends one character before the LiquidJava position
(`getRangeFromPosition` uses `endColumn - 1`), so on the last character
of the error our part shows without the problem part. Pre-existing; left
alone.
- Line tags (`x@51`) in the hover's code are shown as the verifier
writes them; #196 renders them as subscripts in the panel only.

## Tests
- `utils/message-markdown.spec.ts`: code spans incl. a multi-backtick
and a padded span, the link at the reference's `start`, escaping of `* <
_ | #`; call sequences as options; a diagnostic's headline, then notes,
then counterexample, then hints; the headline alone when it has nothing
else.
- `LJDiagnosticsHandlerTest`: the diagnostic's message is the title
alone.
- Client: `npm run test:unit` (140 passed), `npm run test:typecheck`,
`npm run lint`, `npx tsc --noEmit`. Server: `mvn -B test
-Dtest=LJDiagnosticsHandlerTest`.
- Rebased on `main` (after #196); the conflict in
`webview/message-text.ts` resolved as described in the overlap note of
the first version.

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

---------

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

…r lines (#199)

Closes #195

Names the verifier gives values of the code, such as `#if_condition`,
`#getUndoManager_result` or `#case_condition@74`, now explain themselves
on hover in plain words. When their source line is known, the hover
gives it and a click goes there.

## What the verifier already sends
**No verifier change is needed.** Since 0.0.38 (#196), the error's
translation table is keyed by the name as shown, and it holds a position
for every generated name in the error:
- `#if_condition` → the condition, `#getUndoManager_result` → the call,
`#case_condition@74` → its `case`, and so on.
- Several values of one kind get distinct names (`#case_condition@71` …
`@74`), so they no longer share one entry. The issue's note about this
is out of date.
- In A1_56, all 11 generated names in the 19 steps are in the table.

The Context tab has no translation table. There, the server leaves out
generated variables. This PR adds one field, `generatedPlaces` (name as
shown → place). The server code is in this repo, so this is still a
vscode-only change.

## What the hover says
The text is the title of the name, with "at line N" when the line is
known and "Click to go to it." when the name is a link. Every title ends
with "LiquidJava gives it the name #…".

| Name | Hover |
|---|---|
| `#if_condition` | The condition of the if at line N |
| `#loop_condition` | The condition of the loop at line N |
| `#ternary_condition` | The condition of the ? : at line N |
| `#switch_selector` | The value the switch at line N checks |
| `#case_condition` | Whether the case at line N matches |
| `#try_branch` | Whether the try block at line N runs to its end,
rather than a catch block |
| `#catch_branch` | Whether this catch block of the try at line N runs,
rather than a later one |
| `#array_length` | The length of the array created at line N |
| `#new_File` | The new File object created at line N |
| `#size_result` | The value returned by the call to size() at line N |
| `#count_value` | The value of the field count read at line N |
| `#operation_result` | The result of the operation at line N |
| `#expression_value` | The value of the expression at line N |

**Where the line comes from:**
- First, the error's translation table (the Context tab uses
`generatedPlaces`). The name is then a link.
- Otherwise, the name's line tag (`@74`). The line is shown, but the
name is not a link.
- Otherwise, the line is left out.

**`extended#1`** is not a generated name. It is a line tag with no line,
on a program variable, and #196 already explains it ("the 1st value of
extended (line unknown)").

## Where
- **Expected.**
- **Found steps:**
- the binder column: the title of `∀#if_condition` was "Go to source
(boolean)"; it is now the explanation, and the click still highlights
the source;
  - the predicates.
- **The step diff:** both the changed fragments and the unchanged
tokens.
- **The counterexample.**
- **The Context tab's refinements.**

The names have a dotted underline, like the binders, and a pointer
cursor when they are links. A link uses the same `location-link` click
as the message references from #193.

## Screenshots
A1_56 EditCommand, Found at step 7/20, in headless VS Code
(openvscode-server) with verifier 0.0.38.

**Headless screenshots do not capture native tooltips.** The box under
the name is drawn by the screenshot script from the element's real
`title` attribute. On main, the same box shows "(no tooltip)" for the
predicate and "Go to source (boolean)" for the binder.

| | before (main) | after |
|---|---|---|
| `#getUndoManager_result` in a predicate, dark |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-before-dark.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-after-dark.png)
|
| `∀#if_condition` binder, dark |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-before-dark.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-after-dark.png)
|
| `#getUndoManager_result`, light |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-before-light.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-predicate-after-light.png)
|
| `∀#if_condition` binder, light |
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-before-light.png)
|
![](https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/195/A1_56-binder-after-light.png)
|

There is no Context tab screenshot. In A1_56, the Context tab replaces
each generated value by its expression or drops it, so no generated name
is left to show. The unit test covers the Context tab.

## Changes
- `client/src/webview/generated-names.ts` (new): the kinds and their
wording, the hover text, and the rendered name.
- `highlighting.ts`: the highlighter takes an optional `places` table
(name → place). A generated name, together with its line tag, is
rendered by `renderGeneratedName`.
- `vc-changes.ts`, `errors.ts`, `counterexample.ts`, `context/*.ts`:
pass the table through. `renderBinder` uses the explanation as its
title.
- Server: `ContextHistoryDTO.generatedPlaces`, filled by
`ContextHistoryConverter`.

## Tests
- `vc-changes.spec`: one test, which fails on main. It checks:
  - a binder linked through the table;
- a predicate name that is linked, one with no place, and one with only
a tag line;
  - `#ret`, which is left alone;
  - a binder with only a tag;
  - the diff path.
- `context.spec`: one test, which fails on main: a refinement's name
linked through `generatedPlaces`.
- `ContextHistoryConverterTest`: `#array_length` of the Door fixture has
its place.
- Local runs:
  - `npm run test:unit` (142), `test:typecheck`, `lint`;
  - `mvn -B package` (45);
  - `VSCODE_TEST_VERSION=minimum xvfb-run -a npm test` (9 + 1 passing).

## Not in this PR
- The headline message (`found … #getUndoManager_result …`) and the
editor hover are markdown or plain text with no translation table, so
their names are not explained.
- `#ret` (a method's return value) is not one of the verifier's
generated kinds and is left as is.
- A method named `operation` or a field named `expression` would be
described as an operation result or expression value, because the
verifier names them alike.

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

---------

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