GeezerVison

…194)

Fixes the integration failure on main after #191 (stable) and the
earlier ones on #189 (minimum) and #193 (both). Each time it was the
same test timing out: `smoke.test.ts` › "activates, becomes ready, and
verifies its isolated fixture".

## Cause

The server only verifies when the first file of the workspace is opened
(`LJDiagnosticsService.didOpen`). In the `failing` fixture,
`state-errors.test.ts` runs first and opens and verifies the fixture.
The smoke test then opens `FailingRefinement.java` and waits for a
verification that the server never starts. It passed only when a late
notification from the earlier test happened to arrive while it waited,
which is why it failed on some runs and VS Code versions and not others.

## Change

The smoke test waits for the verification on open only when the fixture
has not been verified yet. It still runs the manual `liquidjava.verify`
and checks its result as before.

## Tests

- With a 5 s pause at the start of the smoke test, so every earlier
notification has arrived: main times out exactly as in CI; this branch
passes.
- Without the pause: `xvfb-run -a npm test` (VS Code 1.82, the minimum)
passes twice in a row, 9 + 1 tests; `test:typecheck` and `lint` pass.

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

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