GeezerVison

#493)

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()` (#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](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>