[CatarinaGamboa]

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
∀#if_condition binder, dark
#getUndoManager_result, light
∀#if_condition binder, light

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

[CatarinaGamboa]

Codex review, round 1 (codex exec, run locally on the branch before the first push)

• [vc-changes.ts:48] A generated binder such as #case_condition@74 loses its line in the hover when the translation table has no position: the code strips @74 but never passes it on.

Fixed in 1e96c37: lineOfTag (in highlighting.ts) gives the tag's line to both the binder and the predicate names. The vc-changes.spec test now checks a tag-only binder.

Codex review, round 2 (on 1e96c37): No findings.

[CatarinaGamboa]

Clean-code review (clean-code-principles skill, on this PR's own code)

• vc-changes.ts renderBinder / generated-names.ts - [core-dry] The binder repeated the hover wording and the 0-based to 1-based line logic. Fixed before pushing: both call generatedNameTitle, and explain is private.
• generated-names.ts - [core-fail-fast] kind in NAMED_VALUES on an object literal would have matched prototype keys (#toString would have become a function). Fixed: it is a Map.
• highlighting.ts - [func-few-arguments] An optional places parameter is threaded through four renderers. Declined: a module-level table or a renderer object would be a larger change than this PR needs, and the other choice, a DOM pass after rendering, hides the dependency.
• ContextHistoryConverter.convertGeneratedPlaces - [solid-srp] It sits next to convertVariables and uses the same display. No change.