GeezerVison is showing github.com — Variable superscripts match nothing in the code and render as separate digits · Issue #492 · liquid-java/liquidjava
Variable superscripts match nothing in the code and render as separate digits #492DescriptionImpact: every variable in a message, counterexample and the VS Code panel carries an instance counter (box¹⁵, getBox¹³, size()³). The numbers come from a verifier-wide counter, so they match nothing in the reader's code, and they are shown even when the error has only one instance of that variable. They also render badly: ¹, ², ³ come from the Latin-1 block and ⁰, ⁴–⁹ from the Superscripts block, and many fonts draw them at different heights and widths, so ¹² reads like 1 2 or as two separate marks.
Examples (main, study exercises from #480):
State Refinement Error: expected full(box¹⁵) but could not prove it
Refinement Error: size()³ >= 0 is not a subtype of size()³ > 0
--> Counterexample: size()³ == 0
Here box and size() each have a single instance in the error, so box and size() would say the same thing.
Expected:
- Drop the superscript when the error shows only one instance of a name (message, counterexample, and the panel's Found).
- When several instances must be told apart, number them in a way that relates to the code or at least is small and stable (e.g.
x, x′, x″, or x₁, x₂ per error, or the line, as Change instance variable numbers for line numbers instead of counter #132 / PR Change instance variable numbers for line numbers instead of counter. Refs #132 #271 proposed), and renders consistently.
- Keep names unambiguous: two different instances must never print the same (e.g.
next(), next() in one call).
Where: the counters are added in the verifier (VariableFormatter.toSuperscript); the extension's webview highlighting and diffing match ⁰-⁹ in identifiers (client/src/webview/highlighting.ts, client/src/webview/views/diagnostics/vc-changes.ts), and the hover/context view shows the same names. The fix may belong in the verifier, the extension, or both.
Related: #186 (introduced the superscripts), #132 and PR #271 (line numbers instead of a counter). ActivityCatarinaGamboa commented on Nov 5, 2026 CollaboratorAuthor More actions Design proposal (updated with PM feedback)
Scope. Only the presentation of errors changes: the message, counterexample, hints, and the expected/Found/steps sent to the IDE. Verification, internal names, counters, the translation table and the context view stay the same.
1. Study exercises (main @ 9aa2467)
I ran the verifier on the six exercises of exercises-oss/vscode/proposal-C-stars, on the other proposals (A, B, D), and on the six X/Y fixtures in liquidjava-dev/fixtures/study-exercises. Each project produces one error per exercise.
| Exercise |
Names with a counter today |
2+ instances of a name in the message/counterexample |
Line separates them? |
#k needed? |
| C · A1_01 SlideRecoder |
1 (wParam²⁹⁷) |
no |
– |
no |
| C · A1_19 AccessKeyGenerator |
1 (#randomUUID_result³⁸¹) |
no |
– |
no |
| C · A1_56 EditCommand |
1 (undoManager⁵⁵⁷) |
no. Panel only: 3 × #operation_result, 2 × #if_condition |
yes: the latest stays plain and the others are tagged @41 and @56 (two are on line 56, but only one of them gets a tag) |
no |
| C · A1_09 PlayfieldWindow |
1 (host⁷⁴⁹) |
no |
– |
no |
| C · A1_17 InterruptManager |
1 (this.interrupts⁸⁸⁰) |
no |
– |
no |
| C · A2_04 VmwareCimProbe |
0 |
no |
– |
no |
| A/B/D (another 13 errors) |
1–2 each |
no. Panel only: B · A3_05 iwparam (lines 91/92), D · A1_38 #try_branch (127/151) |
yes |
no |
| X/Y · A1_10, A1_11, A2_04, A3_04 |
1 each |
no |
– |
no |
| X/Y · A2_08 LogWindow |
3 (toIndex, fromIndex, BANNER_LINES) |
no |
– |
no |
| X/Y · A3_07 ScannerOutputStage |
1 (preview) |
yes: preview before and after setTilingMode and setCompressionType |
yes (lines 50/51/54, and 53 in the panel) |
no |
So every study error but one would show only plain names. The exception is A3_07: found startTiling(preview@51) && state2(preview@51) == state2(preview@50) && compressionSet(preview) && state1(preview) == state1(preview@51) but expected tilingExplicit(preview) || tilingSet(preview). The #k fallback is never needed in the study exercises. (Across the whole testSuite, 11 of 437 errors show two instances in the message. Same-line updates such as s-- and b = -b need #k.)
2. Naming rule (per error, one map for message, counterexample, hints and every step)
- A name with one instance in the error is shown plain (
box, size()).
- A name with several instances: the latest instance shown in the message stays plain, which means "current value". Each other instance gets the line it comes from, from the translation table:
x@12.
- Only when two tagged instances would still print the same (same line, or no line in this file):
x@12#1, x@12#2.
3. Rendering
- Verifier, CLI and Problems panel: emit the plain ASCII tag
x@12. @ cannot appear in a Java identifier, so a tag never clashes with a real name. "Copy diagnostic" copies the ASCII text.
- Webview: feasible with one change. Every expression in the panel (expected, Found, steps, counterexample) is rendered by
renderHighlightedContent in client/src/webview/highlighting.ts, which is used at 19 call sites. One extra rule there can render the tag @12 as <sub class="lj-instance" title="value of x at line 12">l12</sub>. The step diff tokenizer TOKEN_PATTERN in client/src/webview/views/diagnostics/vc-changes.ts must keep x@12#2 as one token. Both regexes drop ⁰-⁹.
- Hover:
client/src/services/hover.ts uses appendCodeblock without supportHtml, and it only shows context refinements. It is out of scope and unchanged.
- Structured DTO: not needed. The server already keys the DTO translation table by the display name. If it keys it by the per-error label, the webview gets label → file and line, for the tooltip and click-to-source, from data it already has. The tag can be parsed from text because it always has the form
@digits. Sending each step's predicate as structured tokens instead would rewrite every predicate string and the diff, a much larger change for no gain.
4. Changes
- Verifier: a per-error display-name map, built from the translation table, expected, Found and counterexample.
ExpressionFormatter, VariableFormatter and the hints take the map. The default formatting used by the context view stays as it is today.
- Extension (needs the next verifier release): the server DTOs (binders, step predicates, expected, counterexample, translation-table keys) use the error's map. The webview renders the tag as above.
- Context view, left out for now: it would need the same rule applied within each refinement, with lines from the
VariableDTO positions. It would also need VariableDTO.refinement to stop using the default formatter.
Trade-offs: A merged instance after an if carries the declaration's line. Rule 2 usually makes it the plain current value, so this is rarely visible. Generated names (#operation_result, #if_condition) still read poorly, which is a separate issue.
MetadataMetadataDevelopmentNo branches or pull requestsIssue actions
|