[CatarinaGamboa]

Closes #184. Closes #177.

The Context tab now shows refinements the way the error messages of verifier 0.0.37 do. It works with the released verifier 0.0.37, so no verifier change or release is needed.

What changes

Server (server/src/main/java/dtos/context)

• New ContextDisplay, built once per ContextHistory. It does three things:
  • writes the states of a named set as values of the set, with StateValues.toSetForm: display(host) == notDisplayable instead of notDisplayable(host);
  • names the variables with one DisplayNames for the whole context and ContextHistory.lineOf. Values written alike become host@23, as in error messages, instead of host#1. The declared variable keeps the plain name;
  • stops listing the values the verifier introduces (##switch_selector_N, ##if_condition_N, ...) as variables. If one is always equal to a single expression, that expression replaces it in other rows, so length(data) == #array_length becomes length(data@143) == 1024. If a value has no constraint at all, the facts that mention it are dropped, so cff == #getFileFilter_result disappears.
• VariableDTO gets a displayName. name stays the plain name because hover, autocomplete and the relevant-row marking match it against code identifiers and translation-table keys. Method parameters (MethodDTO) are formatted the same way as before.
• GhostDTO (States of a named @StateSet are shown as plain ghosts (GhostDTO matches stateN by regex) #177): isState is now getParent() != null instead of the state\d+(_) == \d+ regex. A new stateSet holds the set's name, or null when the name is generated (state1), matching when toSetForm keeps the shorthand. Ghosts are sorted so that the states of a set sit together, in the order they are declared.

Client

• The Variables table's Name column shows displayName.
• The Ghosts table writes a state of a named set as compression(ImageWriteParam) == compressionExplicit. Other ghosts and the states of unnamed sets look the same as before.

Screenshots (proposal D, headless VS Code, verifier 0.0.37)

	Before (main)	After
A1_09
A1_38
A1_01, spec file (#177)

Notes

• Overlap with the Found-box work: when a generated value is still shown, it gets the verifier's own display name (DisplayNames/VariableFormatter). If that work renames #case_condition and similar values in the verifier, the Context tab picks up the new names automatically.
• The context history does not keep @RefinementPredicate ghost functions. So toSetForm receives only the state sets as "ghosts". The one case this misses is a state with the same name as a @RefinementPredicate function. That state would be shown in value form, where the verifier keeps the shorthand.
• Path conditions (#if_condition, #case_condition) are no longer rows. Before, they were shown as #case_condition | #switch_selector == BORDERLESS.
• Joined values (after an if or switch, or in a loop) take the line where their variable is declared, which comes from the verifier's placement. That gives host@22#1..#3 in A1_09 and kb@145#2 in A1_38. Error messages name these values the same way.

Checks

npm run test:unit (124 passed), npm run test:typecheck, npm run lint, server mvn -B test (41 passed). Two new server tests and an updated webview spec. Each one fails without this change.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

Full review comments:

• [P2] Keep source refinements separate from display refinements — server/src/main/java/dtos/context/VariableDTO.java:45-46
  When a context variable's refinement refers to a value distinguished by its line number, formatting mainRefinement through ContextDisplay can introduce names such as door@13. The hover and autocomplete providers use mainRefinement to show @Refinement("...") annotations, so they now present annotations that cannot be used as source code. Apply the display formatting to the context-view refinement without replacing the source-form mainRefinement.

• [P2] Sort states by declaration index rather than refinement text — server/src/main/java/utils/ContextHistoryConverter.java:37-39
  For a state set with at least 11 values, lexicographic sorting puts a refinement ending in == 10 before one ending in == 2. The resulting ghost list is not in declaration order, despite the stated intent, and the context view displays that incorrect order. Compare the numeric state index instead of the refinement string.

Both fixed in the next commit: mainRefinement keeps the source form (only refinement and displayName use the context display), and states are sorted by their numeric index within each set.

[CatarinaGamboa]

Codex review, round 2

I found no actionable regressions in the diff. The targeted ContextHistoryConverter tests pass.

Nothing left to fix from Codex.

[CatarinaGamboa]

Clean-code audit (clean-code-principles)

server/src/main/java/dtos/context/ContextDisplay.java:45 - [name-meaningful] `filter(set -> set != null)` reads better as `filter(Objects::nonNull)`
server/src/main/java/dtos/context/ContextDisplay.java:50-77 - [func-small] `of` both collects the names for DisplayNames and sorts generated values into inlinable and unconstrained ones; ~25 lines, one loop
server/src/main/java/utils/ContextHistoryConverter.java:62-67 - [core-encapsulation] `stateIndex` reads the verifier's encoding of a state (`set(_) == index`); verifier 0.0.37 exposes no state index
server/src/main/java/utils/ContextHistoryConverter.java:69-75 + ContextDisplay.java:59 - [core-dry] both decide "generated value" with the same single call, `GeneratedNames.isGenerated`
server/src/main/java/dtos/context/VariableDTO.java:36-37 - [func-few-arguments] the private factory takes the naming and formatting strategies as functions, so method parameters keep their old formatting and context variables use ContextDisplay

Fixed: the first one, in the latest commit.
Left as they are: of is still short, and splitting it would mean passing the half-built maps around. stateIndex has no public alternative in 0.0.37; a GhostState index accessor in the verifier would remove it. The duplicate check is a one-line library call, and wrapping it would add indirection without removing anything. The strategy parameters are deliberate.