[CatarinaGamboa]

Closes #492

Variables in errors no longer carry a superscript counter (box¹⁵). That counter matched nothing in the code, and it mixed Latin-1 ¹²³ with the Superscripts block, which many fonts draw unevenly. Each error now names its variables within one scope:

• A variable that no other variable in the scope is written like keeps its plain name.
• When several are written alike, one keeps the plain name: the declared variable, or else the latest instance the message shows. Each other one gets the line its value comes from, x@12.
• Two tagged variables from the same line (or with no line) are numbered x@12#1, x@12#2. Two different instances never print the same.

The message, counterexample and Found steps of an error share the same names. The context view follows the same rule within each refinement. Verification, internal names, counters and the translation table are unchanged; this is presentation only. toSuperscript is removed.

Before / after

Plain names (A2_10 RandomFailureSupplier, the case reported in the issue):

before: Refinement Error: failures.size()⁸⁴² == size(this.failures) && failures.size()⁸⁴² >= 0 is not a subtype of failures.size()⁸⁴² > 0
         --> Counterexample: failures.size()⁸⁴² == 0
after:  Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0
         --> Counterexample: failures.size() == 0

A3_07 ScannerOutputStage (the only study error with two instances of a name in the message):

before: found startTiling(preview¹¹¹) && state2(preview¹¹¹) == state2(preview¹⁰⁹) && compressionSet(preview¹¹⁶) && state1(preview¹¹⁶) == state1(preview¹¹¹) but expected tilingExplicit(preview¹¹⁶) || tilingSet(preview¹¹⁶)
after:  found startTiling(preview@51) && state2(preview@51) == state2(preview@50) && compressionSet(preview) && state1(preview) == state1(preview@51) but expected tilingExplicit(preview) || tilingSet(preview)

A1_56 EditCommand: the message, and the original Found the panel steps back to:

before: expected redoable(undoManager⁵⁵⁷) but could not prove it
after:  expected redoable(undoManager) but could not prove it

before                                              after
∀#getUndoManager_result⁵⁵⁵ true                     ∀#getUndoManager_result true
∀#operation_result⁵³⁷ true                          ∀#operation_result@41 true
∀#if_condition⁵³⁸ !#operation_result⁵³⁷             ∀#if_condition@41 !#operation_result@41
∀#operation_result⁵⁵⁰ true                          ∀#operation_result@56 true
∀#operation_result⁵⁵¹ true                          ∀#operation_result true
∀#if_condition⁵⁵² !(#operation_result⁵⁵⁰ || …⁵⁵¹)   ∀#if_condition !(#operation_result@56 || #operation_result)
∀undoManager⁵⁵⁷ undoManager⁵⁵⁷ == …⁵⁵⁵               ∀undoManager undoManager == #getUndoManager_result

Across the test suite, 11 of 437 errors still show a tag in the message. All of them are before-and-after values (s--, b = -b, a typestate object across calls). Counters remain only where values on one line must be told apart, e.g. n@11#1 in for (; n > 0; n -= 2);.

API for the extension (liquid-java/vscode-liquidjava#175)

• LJError.getDisplayNames() returns the error's DisplayNames for a RefinementError or StateRefinementError (null for other errors).
  • Binder names, counterexample variables and translation-table keys: names.get(internalName).
  • Expected and the predicate of each step: ExpressionFormatter.format(expression, names).
• Context view: ExpressionFormatter.format(refinement.getExpression(), ContextHistory.getInstance()::lineOf) for VariableDTO.refinement / mainRefinement.
• RefinementError.getFoundAliases() / getExpectedAliases() (Show the definitions of the aliases a refinement error uses #489) use the same names: invocation and expansion are formatted with the error's DisplayNames, so an invocation reads as in Found/Expected, e.g. Below(b@9, 10) with expansion b@9 < 10.
• VariableFormatter.format and ExpressionFormatter.format(expression) keep working without a scope. They write plain names and number clashes within the expression.
• The webview tokenizers should treat name@12#2 as one identifier and can render the tag as <sub>.

Tests

• DisplayNamesTest: line tags with the latest shown value plain; numbering for a shared line or no line, and the declared variable kept plain.
• TestFoundBinders (new Basket.negate fixture): message, counterexample and original Found rows name b@85, b@86 and b alike.
• ContextHistoryTest: the refinement of b after b = -b reads b == b@19 && b > 0.
• Existing assertions on superscripts are updated to plain names where they compare them; assertions that strip superscripts are left as they are.

mvn test (rebased on main after #489): 712 tests, 0 failures. Diff vs main: +353/−113 in 23 files.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

[P2] Resolve context variable lines within the relevant scope (ContextHistory.java): when a launch verifies several methods or files that use the same variable name, lineOf searches every saved local and global variable by name and takes the first match from unordered sets, so format can label an earlier value with a line from a different method or file.

Not relevant, so no change:

• Instance names are unique within a launch. A line is only looked up to tag an instance. Instance names carry the context counter, which is reset once per launch (RefinementProcessor → reinitializeAllContext), and ContextHistory is cleared at every launch. So each #x_N matches exactly one saved variable.
• Declared names are never tagged. A declared name such as b, which can repeat across methods, always keeps the plain name when it appears together with its instances.

Nothing else relevant, so the loop ends here.

[CatarinaGamboa]

Codex review, round 2 (diff rebased on main after #489, with alias expansions named by the error's DisplayNames)

[P2] Resolve context variable lines within the owning class (ContextHistory.java): when an LSP launch processes multiple classes, ContextHistory keeps variables from all of them, while Context.reinitializeAllContext() resets instance counters for each class. Two classes can both have a #x_0 at different lines, and the name-only lookup can pick either.

Not relevant, so no change. This is round 1's finding again, and the premise does not hold: reinitializeAllContext() has one caller, RefinementProcessor.process, which Spoon runs only on the root package (isToBeProcessed returns pkg.isUnnamedPackage()). Packages and classes are then walked from there, so the counter is reset once per launch, not per class. ContextHistory is cleared at the start of every launch. Each #x_N therefore matches one saved variable.

Nothing else relevant, so the loop ends here.

[CatarinaGamboa]

Codex review, round 3 (after the clean-code pass: shared ErrorMessage, one getDisplayNames() on LJError, VCSimplificationResult.getOriginal(), context formatting through ExpressionFormatter)

[P2] Skip unknown lines before selecting a placement (ContextHistory.java): when a saved variable has a placement with an invalid Spoon position, PlacementInCode.getLine() returns null, and findFirst() throws a NullPointerException instead of lineOf() returning unknown. Filter out null lines after the mapping.

Fixed. lineOf now filters null lines after mapping placements to lines, so an invalid position counts as unknown and no longer throws (Stream.findFirst throws on a null element).

Nothing else relevant, so the loop ends here.