GeezerVison

Copy link

Copy Markdown

Collaborator

CatarinaGamboa force-pushed the fix/instance-display-names branch 2 times, most recently from c732fd3 to 275ca17 Compare November 5, 2026 19:37

CatarinaGamboa force-pushed the fix/instance-display-names branch from 275ca17 to 6a3baee Compare November 5, 2026 20:45

1 check passed

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