GeezerVison

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 #…".

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