[CatarinaGamboa]

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 Show the Context tab's refinements as the error messages show them #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 Show the Context tab's refinements as the error messages show them #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)
Found, original (1/10)
Context tab

A2_08 LogWindow, plain names (no change, as for every other study exercise):

before (main)	after

Not in this PR

• Explaining generated names such as #if_condition (Explain the verifier's generated names (#if_condition, call results, …) on hover #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

• List Found as facts and show only readable simplification steps #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).
• Show the code of messages in the editor font and link the lines they name #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

[CatarinaGamboa]

Codex review (codex exec review --base origin/main), run locally before the single push

• Round 1, [P2]: renderLineTags would turn "user@123.com" in a message's code into "userl123.com". Fixed in b78fd6c: string and character literals are skipped. A test was added in diagnostics.spec.
• Round 2, [P2]: the expression highlighter had the same problem, because the grammar has no string-literal rule. Fixed in a8a830c: a literal is one highlighter token and one step-diff token. A test was added in vc-changes.spec.
• Round 3: no actionable findings ("The targeted server test and all 134 client unit tests passed").

[CatarinaGamboa]

Clean-code audit (SOLID / DRY / KISS) of the diff

• vc-changes.ts TOKEN_PATTERN – [core-dry] it repeated the tag and literal grammar of highlighting.ts. Fixed in 53107c5: it is built from the exported LINE_TAG and LITERAL, so the tag grammar has one definition.
• server/.../dtos – [core-kiss] the error's DisplayNames is passed as a parameter to the four DTO factories that need it, with no new types. Only TranslationTableDTO takes null, for errors without names. Kept as is.
• highlighting.ts – [solid-srp] the tag helpers (renderLineTags, withoutLineTag, variableBefore) sit beside the highlighter that uses them, and all of them render expressions. A separate module would only add an import. Kept as is.
• sections.ts renderVariableHighlightButton – [core-dry] the two branches now share one rendered name. Before, the branch without a position wrote raw, unescaped text.
• No (#N) references in source comments. The new comments follow the surrounding style.

Nothing left to change.